Left Termination proof of /tmp/tmpL7Negv/delete-bbf.pl

Left Termination of the query pattern
delete(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇒, 784 ms)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇒, 1190 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 PiDP

        ↳29 PiDPToQDPProof (⇒, 0 ms)

        ↳30 QDP

        ↳31 QDPSizeChangeProof (⇔, 111 ms)

        ↳32 YES

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: delete(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 1 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 2 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\nX6 is free\nX7 is free\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 1 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 2 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 2 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\nX10 is free\nX11 is free\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: delmin(void, T16, T17) | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T9, tree(T9, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: delmin(void, T16, T17), SCOPE: 2, CLAUSE: 5 | delmin(void, T16, T17), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: delmin(void, T16, T17), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ?_2 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="B: ','(less(T26, T26), delete(T26, void, T28))\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="F: less(T26, T26)\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: delete(T26, void, T28)\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: less(T26, T26), SCOPE: 3, CLAUSE: 7 | less(T26, T26), SCOPE: 3, CLAUSE: 8\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: less(T26, T26), SCOPE: 3, CLAUSE: 8\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: less(T31, T31)\n\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(less(T38, T38), delete(T38, void, T40))\n\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(less(T43, T43), delete(T43, void, T45)) | delete(T43, tree(T43, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT43 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T43, tree(T43, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nX94 is free\nX95 is free\nX96 is free\nX97 is free\nX98 is free\ndelete(T9, tree(T9, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))\ndelete(T9, tree(T9, void, void), T3) !=? delete(X94, tree(X95, X96, X97), tree(X95, X98, X97))", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(less(T43, T43), delete(T43, void, T45)), SCOPE: 4, CLAUSE: 7 | ','(less(T43, T43), delete(T43, void, T45)), SCOPE: 4, CLAUSE: 8 | ?_4 | delete(T43, tree(T43, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT43 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T43, tree(T43, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(less(T43, T43), delete(T43, void, T45)), SCOPE: 4, CLAUSE: 8 | ?_4 | delete(T43, tree(T43, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT43 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T43, tree(T43, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(less(T43, T43), delete(T43, void, T45)), SCOPE: 4, CLAUSE: 8\n\nT43 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T43, tree(T43, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ?_4 | delete(T43, tree(T43, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT43 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T43, tree(T43, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="C: ','(less(T50, T50), delete(s(T50), void, T45))\n\nT50 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(s(T50), tree(s(T50), void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: less(T50, T50)\n\nT50 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(s(T50), tree(s(T50), void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: delete(s(T50), void, T45)\n\nT50 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(s(T50), tree(s(T50), void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: delete(T43, tree(T43, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT43 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T43, tree(T43, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(less(T57, T57), delete(T57, void, T59))\n\nT57 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\ndelete(T57, tree(T57, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(less(T62, T62), delete(T62, void, T64))\n\nT62 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nX94 is free\nX95 is free\nX96 is free\nX97 is free\nX98 is free\ndelete(T62, tree(T62, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))\ndelete(T62, tree(T62, void, void), T3) !=? delete(X94, tree(X95, X96, X97), tree(X95, X98, X97))", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(less(T62, T62), delete(T62, void, T64)), SCOPE: 5, CLAUSE: 7 | ','(less(T62, T62), delete(T62, void, T64)), SCOPE: 5, CLAUSE: 8\n\nT62 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nX94 is free\nX95 is free\nX96 is free\nX97 is free\nX98 is free\ndelete(T62, tree(T62, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))\ndelete(T62, tree(T62, void, void), T3) !=? delete(X94, tree(X95, X96, X97), tree(X95, X98, X97))", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(less(T62, T62), delete(T62, void, T64)), SCOPE: 5, CLAUSE: 8\n\nT62 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nX94 is free\nX95 is free\nX96 is free\nX97 is free\nX98 is free\ndelete(T62, tree(T62, void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))\ndelete(T62, tree(T62, void, void), T3) !=? delete(X94, tree(X95, X96, X97), tree(X95, X98, X97))", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(less(T67, T67), delete(s(T67), void, T64))\n\nT67 is ground\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nX94 is free\nX95 is free\nX96 is free\nX97 is free\nX98 is free\ndelete(s(T67), tree(s(T67), void, void), T3) !=? delete(X17, tree(X17, X18, X19), tree(X20, X18, X21))\ndelete(s(T67), tree(s(T67), void, void), T3) !=? delete(X94, tree(X95, X96, X97), tree(X95, X98, X97))", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: delmin(T73, T76, T77) | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 3 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 4\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: delmin(T73, T76, T77), SCOPE: 6, CLAUSE: 5 | delmin(T73, T76, T77), SCOPE: 6, CLAUSE: 6 | ?_6 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 3 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 4\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: delmin(T73, T76, T77), SCOPE: 6, CLAUSE: 5\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: delmin(T73, T76, T77), SCOPE: 6, CLAUSE: 6 | ?_6 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 3 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 4\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: delmin(T73, T76, T77), SCOPE: 6, CLAUSE: 6\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ?_6 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 3 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 4\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="D: delmin(T113, T118, T119)\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: delmin(T113, T118, T119), SCOPE: 7, CLAUSE: 5 | delmin(T113, T118, T119), SCOPE: 7, CLAUSE: 6\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: delmin(T113, T118, T119), SCOPE: 7, CLAUSE: 5\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: delmin(T113, T118, T119), SCOPE: 7, CLAUSE: 6\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: delmin(T147, T152, T153)\n\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 3 | delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 4\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 3\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: delete(T72, tree(T72, void, T73), T3), SCOPE: 1, CLAUSE: 4\n\nT72 is ground\nT73 is ground\nX10 is free\nX11 is free\ndelete(T72, tree(T72, void, T73), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(less(T170, T170), delete(T170, void, T173))\n\nT170 is ground\nT171 is ground\nX10 is free\nX11 is free\ndelete(T170, tree(T170, void, T171), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="E: ','(less(T180, T180), delete(T180, T181, T183))\n\nT180 is ground\nT181 is ground\nX10 is free\nX11 is free\ndelete(T180, tree(T180, void, T181), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: less(T180, T180)\n\nT180 is ground\nT181 is ground\nX10 is free\nX11 is free\ndelete(T180, tree(T180, void, T181), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: delete(T180, T181, T183)\n\nT180 is ground\nT181 is ground\nX10 is free\nX11 is free\ndelete(T180, tree(T180, void, T181), T3) !=? delete(X10, tree(X10, X11, void), X11)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(less(T191, T191), delete(T191, void, T194)) | delete(T191, tree(T191, void, T192), T3), SCOPE: 1, CLAUSE: 4\n\nT191 is ground\nT192 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\nX295 is free\nX296 is free\nX297 is free\nX298 is free\nX299 is free\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X295, tree(X296, X297, X298), tree(X296, X299, X298))", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(less(T191, T191), delete(T191, void, T194)), SCOPE: 8, CLAUSE: 7 | ','(less(T191, T191), delete(T191, void, T194)), SCOPE: 8, CLAUSE: 8 | ?_8 | delete(T191, tree(T191, void, T192), T3), SCOPE: 1, CLAUSE: 4\n\nT191 is ground\nT192 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(less(T191, T191), delete(T191, void, T194)), SCOPE: 8, CLAUSE: 8 | ?_8 | delete(T191, tree(T191, void, T192), T3), SCOPE: 1, CLAUSE: 4\n\nT191 is ground\nT192 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(less(T191, T191), delete(T191, void, T194)), SCOPE: 8, CLAUSE: 8\n\nT191 is ground\nT192 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ?_8 | delete(T191, tree(T191, void, T192), T3), SCOPE: 1, CLAUSE: 4\n\nT191 is ground\nT192 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(less(T199, T199), delete(s(T199), void, T194))\n\nT192 is ground\nT199 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(s(T199), tree(s(T199), void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(s(T199), tree(s(T199), void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: less(T199, T199)\n\nT192 is ground\nT199 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(s(T199), tree(s(T199), void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(s(T199), tree(s(T199), void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: delete(s(T199), void, T194)\n\nT192 is ground\nT199 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(s(T199), tree(s(T199), void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(s(T199), tree(s(T199), void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: delete(T191, tree(T191, void, T192), T3), SCOPE: 1, CLAUSE: 4\n\nT191 is ground\nT192 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T191, tree(T191, void, T192), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(less(T208, T208), delete(T208, T209, T211))\n\nT208 is ground\nT209 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ndelete(T208, tree(T208, void, T209), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T208, tree(T208, void, T209), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(less(T215, T215), delete(T215, T216, T218))\n\nT215 is ground\nT216 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\nX295 is free\nX296 is free\nX297 is free\nX298 is free\nX299 is free\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X295, tree(X296, X297, X298), tree(X296, X299, X298))", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(less(T215, T215), delete(T215, T216, T218)), SCOPE: 9, CLAUSE: 7 | ','(less(T215, T215), delete(T215, T216, T218)), SCOPE: 9, CLAUSE: 8\n\nT215 is ground\nT216 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\nX295 is free\nX296 is free\nX297 is free\nX298 is free\nX299 is free\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X295, tree(X296, X297, X298), tree(X296, X299, X298))", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(less(T215, T215), delete(T215, T216, T218)), SCOPE: 9, CLAUSE: 8\n\nT215 is ground\nT216 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\nX295 is free\nX296 is free\nX297 is free\nX298 is free\nX299 is free\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))\ndelete(T215, tree(T215, void, T216), T3) !=? delete(X295, tree(X296, X297, X298), tree(X296, X299, X298))", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(less(T221, T221), delete(s(T221), T216, T218))\n\nT216 is ground\nT221 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\nX295 is free\nX296 is free\nX297 is free\nX298 is free\nX299 is free\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X295, tree(X296, X297, X298), tree(X296, X299, X298))", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: less(T221, T221)\n\nT216 is ground\nT221 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\nX295 is free\nX296 is free\nX297 is free\nX298 is free\nX299 is free\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X295, tree(X296, X297, X298), tree(X296, X299, X298))", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: delete(s(T221), T216, T218)\n\nT216 is ground\nT221 is ground\nX10 is free\nX11 is free\nX159 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\nX295 is free\nX296 is free\nX297 is free\nX298 is free\nX299 is free\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X10, tree(X10, X11, void), X11)\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X159, tree(X159, X160, X161), tree(X162, X160, X163))\ndelete(s(T221), tree(s(T221), void, T216), T3) !=? delete(X295, tree(X296, X297, X298), tree(X296, X299, X298))", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: true | delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 4\n\nT228 is ground\nT229 is ground\nX6 is free\nX7 is free\ndelete(T228, tree(T228, T229, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 4\n\nT228 is ground\nT229 is ground\nX6 is free\nX7 is free\ndelete(T228, tree(T228, T229, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: delmin(void, T238, T239) | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 4\n\nT234 is ground\nT235 is ground\nX6 is free\nX7 is free\ndelete(T234, tree(T234, T235, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 4\n\nT228 is ground\nT229 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T228, tree(T228, T229, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T228, tree(T228, T229, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: delmin(void, T238, T239), SCOPE: 10, CLAUSE: 5 | delmin(void, T238, T239), SCOPE: 10, CLAUSE: 6 | ?_10 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 4\n\nT234 is ground\nT235 is ground\nX6 is free\nX7 is free\ndelete(T234, tree(T234, T235, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: delmin(void, T238, T239), SCOPE: 10, CLAUSE: 6 | ?_10 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 4\n\nT234 is ground\nT235 is ground\nX6 is free\nX7 is free\ndelete(T234, tree(T234, T235, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ?_10 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 4\n\nT234 is ground\nT235 is ground\nX6 is free\nX7 is free\ndelete(T234, tree(T234, T235, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 4\n\nT234 is ground\nT235 is ground\nX6 is free\nX7 is free\ndelete(T234, tree(T234, T235, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 3\n\nT234 is ground\nT235 is ground\nX6 is free\nX7 is free\ndelete(T234, tree(T234, T235, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: delete(T234, tree(T234, T235, void), T3), SCOPE: 1, CLAUSE: 4\n\nT234 is ground\nT235 is ground\nX6 is free\nX7 is free\ndelete(T234, tree(T234, T235, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(less(T252, T252), delete(T252, T253, T255))\n\nT252 is ground\nT253 is ground\nX6 is free\nX7 is free\ndelete(T252, tree(T252, T253, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: less(T252, T252)\n\nT252 is ground\nT253 is ground\nX6 is free\nX7 is free\ndelete(T252, tree(T252, T253, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: delete(T252, T253, T255)\n\nT252 is ground\nT253 is ground\nX6 is free\nX7 is free\ndelete(T252, tree(T252, T253, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(less(T266, T266), delete(T266, void, T269))\n\nT266 is ground\nT267 is ground\nX6 is free\nX7 is free\ndelete(T266, tree(T266, T267, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(less(T273, T273), delete(T273, T274, T276)) | delete(T273, tree(T273, T274, void), T3), SCOPE: 1, CLAUSE: 4\n\nT273 is ground\nT274 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: delete(T228, tree(T228, T229, void), T3), SCOPE: 1, CLAUSE: 4\n\nT228 is ground\nT229 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\nX438 is free\nX439 is free\nX440 is free\nX441 is free\nX442 is free\ndelete(T228, tree(T228, T229, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T228, tree(T228, T229, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))\ndelete(T228, tree(T228, T229, void), T3) !=? delete(X438, tree(X439, X440, X441), tree(X439, X442, X441))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(less(T273, T273), delete(T273, T274, T276)), SCOPE: 11, CLAUSE: 7 | ','(less(T273, T273), delete(T273, T274, T276)), SCOPE: 11, CLAUSE: 8 | ?_11 | delete(T273, tree(T273, T274, void), T3), SCOPE: 1, CLAUSE: 4\n\nT273 is ground\nT274 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(less(T273, T273), delete(T273, T274, T276)), SCOPE: 11, CLAUSE: 8 | ?_11 | delete(T273, tree(T273, T274, void), T3), SCOPE: 1, CLAUSE: 4\n\nT273 is ground\nT274 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(less(T273, T273), delete(T273, T274, T276)), SCOPE: 11, CLAUSE: 8\n\nT273 is ground\nT274 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ?_11 | delete(T273, tree(T273, T274, void), T3), SCOPE: 1, CLAUSE: 4\n\nT273 is ground\nT274 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(less(T281, T281), delete(s(T281), T274, T276))\n\nT274 is ground\nT281 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(s(T281), tree(s(T281), T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T281), tree(s(T281), T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: less(T281, T281)\n\nT274 is ground\nT281 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(s(T281), tree(s(T281), T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T281), tree(s(T281), T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: delete(s(T281), T274, T276)\n\nT274 is ground\nT281 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(s(T281), tree(s(T281), T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T281), tree(s(T281), T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: delete(T273, tree(T273, T274, void), T3), SCOPE: 1, CLAUSE: 4\n\nT273 is ground\nT274 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T273, tree(T273, T274, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(less(T292, T292), delete(T292, void, T295))\n\nT292 is ground\nT293 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\ndelete(T292, tree(T292, T293, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T292, tree(T292, T293, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(less(T299, T299), delete(T299, void, T302))\n\nT299 is ground\nT300 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\nX438 is free\nX439 is free\nX440 is free\nX441 is free\nX442 is free\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X438, tree(X439, X440, X441), tree(X439, X442, X441))", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(less(T299, T299), delete(T299, void, T302)), SCOPE: 12, CLAUSE: 7 | ','(less(T299, T299), delete(T299, void, T302)), SCOPE: 12, CLAUSE: 8\n\nT299 is ground\nT300 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\nX438 is free\nX439 is free\nX440 is free\nX441 is free\nX442 is free\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X438, tree(X439, X440, X441), tree(X439, X442, X441))", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(less(T299, T299), delete(T299, void, T302)), SCOPE: 12, CLAUSE: 8\n\nT299 is ground\nT300 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\nX438 is free\nX439 is free\nX440 is free\nX441 is free\nX442 is free\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X438, tree(X439, X440, X441), tree(X439, X442, X441))", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(less(T305, T305), delete(s(T305), void, T302))\n\nT300 is ground\nT305 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\nX438 is free\nX439 is free\nX440 is free\nX441 is free\nX442 is free\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X438, tree(X439, X440, X441), tree(X439, X442, X441))", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: less(T305, T305)\n\nT300 is ground\nT305 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\nX438 is free\nX439 is free\nX440 is free\nX441 is free\nX442 is free\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X438, tree(X439, X440, X441), tree(X439, X442, X441))", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: delete(s(T305), void, T302)\n\nT300 is ground\nT305 is ground\nX6 is free\nX7 is free\nX370 is free\nX371 is free\nX372 is free\nX373 is free\nX374 is free\nX438 is free\nX439 is free\nX440 is free\nX441 is free\nX442 is free\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X370, tree(X370, X371, X372), tree(X373, X371, X374))\ndelete(s(T305), tree(s(T305), T300, void), T3) !=? delete(X438, tree(X439, X440, X441), tree(X439, X442, X441))", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: delmin(T315, T318, T319) | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 3 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 4\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T1, T2, T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: delmin(T315, T318, T319), SCOPE: 13, CLAUSE: 5 | delmin(T315, T318, T319), SCOPE: 13, CLAUSE: 6 | ?_13 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 3 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 4\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: delmin(T315, T318, T319), SCOPE: 13, CLAUSE: 5\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: delmin(T315, T318, T319), SCOPE: 13, CLAUSE: 6 | ?_13 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 3 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 4\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: delmin(T315, T318, T319), SCOPE: 13, CLAUSE: 6\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ?_13 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 3 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 4\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: delmin(T355, T360, T361)\n\nT313 is ground\nT314 is ground\nT354 is ground\nT355 is ground\nT356 is ground\nX6 is free\nX7 is free\ndelete(T313, tree(T313, T314, tree(T354, T355, T356)), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 3 | delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 4\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 3\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: delete(T313, tree(T313, T314, T315), T3), SCOPE: 1, CLAUSE: 4\n\nT313 is ground\nT314 is ground\nT315 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T313, tree(T313, T314, T315), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(less(T382, T382), delete(T382, T383, T386))\n\nT382 is ground\nT383 is ground\nT384 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T382, tree(T382, T383, T384), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T382, tree(T382, T383, T384), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: less(T382, T382)\n\nT382 is ground\nT383 is ground\nT384 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T382, tree(T382, T383, T384), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T382, tree(T382, T383, T384), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: delete(T382, T383, T386)\n\nT382 is ground\nT383 is ground\nT384 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T382, tree(T382, T383, T384), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T382, tree(T382, T383, T384), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(less(T399, T399), delete(T399, T401, T403))\n\nT399 is ground\nT400 is ground\nT401 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T399, tree(T399, T400, T401), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T399, tree(T399, T400, T401), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: less(T399, T399)\n\nT399 is ground\nT400 is ground\nT401 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T399, tree(T399, T400, T401), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T399, tree(T399, T400, T401), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: delete(T399, T401, T403)\n\nT399 is ground\nT400 is ground\nT401 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\ndelete(T399, tree(T399, T400, T401), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T399, tree(T399, T400, T401), T3) !=? delete(X363, tree(X363, X364, void), X364)", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(less(T413, T414), delete(T413, T415, T418)) | delete(T413, tree(T414, T415, T416), T3), SCOPE: 1, CLAUSE: 4\n\nT413 is ground\nT414 is ground\nT415 is ground\nT416 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T1, T2, T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(T1, T2, T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(less(T413, T414), delete(T413, T415, T418)), SCOPE: 14, CLAUSE: 7 | ','(less(T413, T414), delete(T413, T415, T418)), SCOPE: 14, CLAUSE: 8 | ?_14 | delete(T413, tree(T414, T415, T416), T3), SCOPE: 1, CLAUSE: 4\n\nT413 is ground\nT414 is ground\nT415 is ground\nT416 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(less(T413, T414), delete(T413, T415, T418)), SCOPE: 14, CLAUSE: 7\n\nT413 is ground\nT414 is ground\nT415 is ground\nT416 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(less(T413, T414), delete(T413, T415, T418)), SCOPE: 14, CLAUSE: 8 | ?_14 | delete(T413, tree(T414, T415, T416), T3), SCOPE: 1, CLAUSE: 4\n\nT413 is ground\nT414 is ground\nT415 is ground\nT416 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: delete(0, T415, T418)\n\nT415 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(less(T413, T414), delete(T413, T415, T418)), SCOPE: 14, CLAUSE: 8\n\nT413 is ground\nT414 is ground\nT415 is ground\nT416 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ?_14 | delete(T413, tree(T414, T415, T416), T3), SCOPE: 1, CLAUSE: 4\n\nT413 is ground\nT414 is ground\nT415 is ground\nT416 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(less(T434, T435), delete(s(T434), T415, T418))\n\nT415 is ground\nT416 is ground\nT434 is ground\nT435 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="G: less(T434, T435)\n\nT415 is ground\nT416 is ground\nT434 is ground\nT435 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: delete(s(T434), T415, T418)\n\nT415 is ground\nT416 is ground\nT434 is ground\nT435 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: less(T434, T435), SCOPE: 15, CLAUSE: 7 | less(T434, T435), SCOPE: 15, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT434 is ground\nT435 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: less(T434, T435), SCOPE: 15, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT434 is ground\nT435 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: less(T434, T435), SCOPE: 15, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT434 is ground\nT435 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T434), tree(s(T435), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: less(T449, T450)\n\nT415 is ground\nT416 is ground\nT449 is ground\nT450 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: less(T449, T450), SCOPE: 16, CLAUSE: 7 | less(T449, T450), SCOPE: 16, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT449 is ground\nT450 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: less(T449, T450), SCOPE: 16, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT449 is ground\nT450 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: less(T449, T450), SCOPE: 16, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT449 is ground\nT450 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(T449)), tree(s(s(T450)), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: less(T462, T463)\n\nT415 is ground\nT416 is ground\nT462 is ground\nT463 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: less(T462, T463), SCOPE: 17, CLAUSE: 7 | less(T462, T463), SCOPE: 17, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT462 is ground\nT463 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: less(T462, T463), SCOPE: 17, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT462 is ground\nT463 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: less(T462, T463), SCOPE: 17, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT462 is ground\nT463 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(T462))), tree(s(s(s(T463))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: less(T475, T476)\n\nT415 is ground\nT416 is ground\nT475 is ground\nT476 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: less(T475, T476), SCOPE: 18, CLAUSE: 7 | less(T475, T476), SCOPE: 18, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT475 is ground\nT476 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: less(T475, T476), SCOPE: 18, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT475 is ground\nT476 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: less(T475, T476), SCOPE: 18, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT475 is ground\nT476 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(T475)))), tree(s(s(s(s(T476)))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: less(T488, T489)\n\nT415 is ground\nT416 is ground\nT488 is ground\nT489 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: less(T488, T489), SCOPE: 19, CLAUSE: 7 | less(T488, T489), SCOPE: 19, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT488 is ground\nT489 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: less(T488, T489), SCOPE: 19, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT488 is ground\nT489 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: less(T488, T489), SCOPE: 19, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT488 is ground\nT489 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(T488))))), tree(s(s(s(s(s(T489))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: less(T501, T502)\n\nT415 is ground\nT416 is ground\nT501 is ground\nT502 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: less(T501, T502), SCOPE: 20, CLAUSE: 7 | less(T501, T502), SCOPE: 20, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT501 is ground\nT502 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: less(T501, T502), SCOPE: 20, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT501 is ground\nT502 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: less(T501, T502), SCOPE: 20, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT501 is ground\nT502 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(T501)))))), tree(s(s(s(s(s(s(T502)))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: less(T514, T515)\n\nT415 is ground\nT416 is ground\nT514 is ground\nT515 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: less(T514, T515), SCOPE: 21, CLAUSE: 7 | less(T514, T515), SCOPE: 21, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT514 is ground\nT515 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: less(T514, T515), SCOPE: 21, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT514 is ground\nT515 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: less(T514, T515), SCOPE: 21, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT514 is ground\nT515 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(s(T514))))))), tree(s(s(s(s(s(s(s(T515))))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: less(T527, T528)\n\nT415 is ground\nT416 is ground\nT527 is ground\nT528 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(s(s(s(s(s(s(s(s(T527)))))))), tree(s(s(s(s(s(s(s(s(T528)))))))), T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(s(T527)))))))), tree(s(s(s(s(s(s(s(s(T528)))))))), T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(s(s(s(s(s(s(s(T527)))))))), tree(s(s(s(s(s(s(s(s(T528)))))))), T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="H: less(T527, T528)\n\nT527 is ground\nT528 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: less(T527, T528), SCOPE: 22, CLAUSE: 7 | less(T527, T528), SCOPE: 22, CLAUSE: 8\n\nT527 is ground\nT528 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: less(T527, T528), SCOPE: 22, CLAUSE: 7\n\nT527 is ground\nT528 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: less(T527, T528), SCOPE: 22, CLAUSE: 8\n\nT527 is ground\nT528 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: less(T544, T545)\n\nT544 is ground\nT545 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: delete(T413, tree(T414, T415, T416), T3), SCOPE: 1, CLAUSE: 4\n\nT413 is ground\nT414 is ground\nT415 is ground\nT416 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T413, tree(T414, T415, T416), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: ','(less(T563, T562), delete(T562, T565, T567))\n\nT562 is ground\nT563 is ground\nT564 is ground\nT565 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: less(T563, T562)\n\nT562 is ground\nT563 is ground\nT564 is ground\nT565 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: delete(T562, T565, T567)\n\nT562 is ground\nT563 is ground\nT564 is ground\nT565 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T562, tree(T563, T564, T565), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: ','(less(T582, T581), delete(T581, T584, T586))\n\nT581 is ground\nT582 is ground\nT583 is ground\nT584 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(less(T582, T581), delete(T581, T584, T586)), SCOPE: 23, CLAUSE: 7 | ','(less(T582, T581), delete(T581, T584, T586)), SCOPE: 23, CLAUSE: 8\n\nT581 is ground\nT582 is ground\nT583 is ground\nT584 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: ','(less(T582, T581), delete(T581, T584, T586)), SCOPE: 23, CLAUSE: 7\n\nT581 is ground\nT582 is ground\nT583 is ground\nT584 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: ','(less(T582, T581), delete(T581, T584, T586)), SCOPE: 23, CLAUSE: 8\n\nT581 is ground\nT582 is ground\nT583 is ground\nT584 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(T581, tree(T582, T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: delete(s(T591), T584, T586)\n\nT583 is ground\nT584 is ground\nT591 is ground\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(s(T591), tree(0, T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: ','(less(T600, T601), delete(s(T601), T584, T586))\n\nT583 is ground\nT584 is ground\nT600 is ground\nT601 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: less(T600, T601)\n\nT583 is ground\nT584 is ground\nT600 is ground\nT601 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: delete(s(T601), T584, T586)\n\nT583 is ground\nT584 is ground\nT600 is ground\nT601 is ground\nX6 is free\nX7 is free\nX363 is free\nX364 is free\nX509 is free\nX510 is free\nX511 is free\nX512 is free\nX513 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free\nX623 is free\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X363, tree(X363, X364, void), X364)\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X509, tree(X509, X510, X511), tree(X512, X510, X513))\ndelete(s(T601), tree(s(T600), T583, T584), T3) !=? delete(X619, tree(X620, X621, X622), tree(X620, X623, X622))", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 251 [arrowhead = none ];
251 -> 2;

252 [label="EVAL with clause\ndelete(X6, tree(X6, void, X7), X7).\nand substitutionT1 -> T6,\nX6 -> T6,\nX7 -> T7,\nT2 -> tree(T6, void, T7),\nT3 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 252 [arrowhead = none ];
252 -> 3;

253 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 253 [arrowhead = none ];
253 -> 4;

254 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 254 [arrowhead = none ];
254 -> 5;

255 [label="EVAL with clause\ndelete(X363, tree(X363, X364, void), X364).\nand substitutionT1 -> T228,\nX363 -> T228,\nX364 -> T229,\nT2 -> tree(T228, T229, void),\nT3 -> T229", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 255 [arrowhead = none ];
255 -> 96;

256 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 256 [arrowhead = none ];
256 -> 97;

257 [label="EVAL with clause\ndelete(X10, tree(X10, X11, void), X11).\nand substitutionT6 -> T9,\nX10 -> T9,\nX11 -> void,\nT7 -> void,\nT3 -> void", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 257 [arrowhead = none ];
257 -> 6;

258 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 258 [arrowhead = none ];
258 -> 7;

259 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 259 [arrowhead = none ];
259 -> 8;

260 [label="EVAL with clause\ndelete(X159, tree(X159, X160, X161), tree(X162, X160, X163)) :- delmin(X161, X162, X163).\nand substitutionT6 -> T72,\nX159 -> T72,\nX160 -> void,\nT7 -> T73,\nX161 -> T73,\nX162 -> T76,\nX163 -> T77,\nT3 -> tree(T76, void, T77),\nT74 -> T76,\nT75 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 260 [arrowhead = none ];
260 -> 46;

261 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 261 [arrowhead = none ];
261 -> 47;

262 [label="EVAL with clause\ndelete(X17, tree(X17, X18, X19), tree(X20, X18, X21)) :- delmin(X19, X20, X21).\nand substitutionT9 -> T13,\nX17 -> T13,\nX18 -> void,\nX19 -> void,\nX20 -> T16,\nX21 -> T17,\nT3 -> tree(T16, void, T17),\nT14 -> T16,\nT15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 262 [arrowhead = none ];
262 -> 9;

263 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 263 [arrowhead = none ];
263 -> 10;

264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
9 -> 264 [arrowhead = none ];
264 -> 11;

265 [label="EVAL with clause\ndelete(X94, tree(X95, X96, X97), tree(X95, X98, X97)) :- ','(less(X94, X95), delete(X94, X96, X98)).\nand substitutionT9 -> T43,\nX94 -> T43,\nX95 -> T43,\nX96 -> void,\nX97 -> void,\nX98 -> T45,\nT3 -> tree(T43, T45, void),\nT44 -> T45", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 265 [arrowhead = none ];
265 -> 27;

266 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 266 [arrowhead = none ];
266 -> 28;

267 [label="BACKTRACK\nfor clause: delmin(tree(Y, void, Right), Y, Right)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 267 [arrowhead = none ];
267 -> 12;

268 [label="BACKTRACK\nfor clause: delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 268 [arrowhead = none ];
268 -> 13;

269 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 269 [arrowhead = none ];
269 -> 14;

270 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 270 [arrowhead = none ];
270 -> 15;

271 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 271 [arrowhead = none ];
271 -> 16;

272 [label="EVAL with clause\ndelete(X50, tree(X51, X52, X53), tree(X51, X54, X53)) :- ','(less(X50, X51), delete(X50, X52, X54)).\nand substitutionT13 -> T26,\nX50 -> T26,\nX51 -> T26,\nX52 -> void,\nX53 -> void,\nX54 -> T28,\nT3 -> tree(T26, T28, void),\nT27 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 272 [arrowhead = none ];
272 -> 17;

273 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 273 [arrowhead = none ];
273 -> 18;

274 [label="EVAL with clause\ndelete(X82, tree(X83, X84, X85), tree(X83, X84, X86)) :- ','(less(X83, X82), delete(X82, X85, X86)).\nand substitutionT13 -> T38,\nX82 -> T38,\nX83 -> T38,\nX84 -> void,\nX85 -> void,\nX86 -> T40,\nT3 -> tree(T38, void, T40),\nT39 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 274 [arrowhead = none ];
274 -> 25;

275 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 275 [arrowhead = none ];
275 -> 26;

276 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 276 [arrowhead = none ];
276 -> 19;

277 [label="SPLIT 2\nnew knowledge:\nT26 is ground", fontsize=14, style = filled, fillcolor = violet];
17 -> 277 [arrowhead = none ];
277 -> 20;

278 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 278 [arrowhead = none ];
278 -> 21;

279 [label="INSTANCE with matching:\nT1 -> T26\nT2 -> void\nT3 -> T28", fontsize=14, style = filled, fillcolor = lightgrey];
20 -> 279 [arrowhead = none , style=dashed];
279 -> 1[style=dashed];

280 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 280 [arrowhead = none ];
280 -> 22;

281 [label="EVAL with clause\nless(s(X64), s(X65)) :- less(X64, X65).\nand substitutionX64 -> T31,\nT26 -> s(T31),\nX65 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 281 [arrowhead = none ];
281 -> 23;

282 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 282 [arrowhead = none ];
282 -> 24;

283 [label="INSTANCE with matching:\nT26 -> T31", fontsize=14, style = filled, fillcolor = lightgrey];
23 -> 283 [arrowhead = none , style=dashed];
283 -> 19[style=dashed];

284 [label="INSTANCE with matching:\nT26 -> T38\nT28 -> T40", fontsize=14, style = filled, fillcolor = lightgrey];
25 -> 284 [arrowhead = none , style=dashed];
284 -> 17[style=dashed];

285 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 285 [arrowhead = none ];
285 -> 29;

286 [label="EVAL with clause\ndelete(X140, tree(X141, X142, X143), tree(X141, X142, X144)) :- ','(less(X141, X140), delete(X140, X143, X144)).\nand substitutionT9 -> T62,\nX140 -> T62,\nX141 -> T62,\nX142 -> void,\nX143 -> void,\nX144 -> T64,\nT3 -> tree(T62, void, T64),\nT63 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 286 [arrowhead = none ];
286 -> 40;

287 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 287 [arrowhead = none ];
287 -> 41;

288 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 288 [arrowhead = none ];
288 -> 30;

289 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 289 [arrowhead = none ];
289 -> 31;

290 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 290 [arrowhead = none ];
290 -> 32;

291 [label="EVAL with clause\nless(s(X108), s(X109)) :- less(X108, X109).\nand substitutionX108 -> T50,\nT43 -> s(T50),\nX109 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 291 [arrowhead = none ];
291 -> 33;

292 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 292 [arrowhead = none ];
292 -> 34;

293 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 293 [arrowhead = none ];
293 -> 37;

294 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
33 -> 294 [arrowhead = none ];
294 -> 35;

295 [label="SPLIT 2\nnew knowledge:\nT50 is ground", fontsize=14, style = filled, fillcolor = violet];
33 -> 295 [arrowhead = none ];
295 -> 36;

296 [label="INSTANCE with matching:\nT26 -> T50", fontsize=14, style = filled, fillcolor = lightgrey];
35 -> 296 [arrowhead = none , style=dashed];
296 -> 19[style=dashed];

297 [label="INSTANCE with matching:\nT1 -> s(T50)\nT2 -> void\nT3 -> T45", fontsize=14, style = filled, fillcolor = lightgrey];
36 -> 297 [arrowhead = none , style=dashed];
297 -> 1[style=dashed];

298 [label="EVAL with clause\ndelete(X128, tree(X129, X130, X131), tree(X129, X130, X132)) :- ','(less(X129, X128), delete(X128, X131, X132)).\nand substitutionT43 -> T57,\nX128 -> T57,\nX129 -> T57,\nX130 -> void,\nX131 -> void,\nX132 -> T59,\nT3 -> tree(T57, void, T59),\nT58 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 298 [arrowhead = none ];
298 -> 38;

299 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 299 [arrowhead = none ];
299 -> 39;

300 [label="INSTANCE with matching:\nT26 -> T57\nT28 -> T59", fontsize=14, style = filled, fillcolor = lightgrey];
38 -> 300 [arrowhead = none , style=dashed];
300 -> 17[style=dashed];

301 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 301 [arrowhead = none ];
301 -> 42;

302 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 302 [arrowhead = none ];
302 -> 43;

303 [label="EVAL with clause\nless(s(X150), s(X151)) :- less(X150, X151).\nand substitutionX150 -> T67,\nT62 -> s(T67),\nX151 -> T67", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 303 [arrowhead = none ];
303 -> 44;

304 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 304 [arrowhead = none ];
304 -> 45;

305 [label="INSTANCE with matching:\nT50 -> T67\nT45 -> T64", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 305 [arrowhead = none , style=dashed];
305 -> 33[style=dashed];

306 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
46 -> 306 [arrowhead = none ];
306 -> 48;

307 [label="EVAL with clause\ndelete(X295, tree(X296, X297, X298), tree(X296, X299, X298)) :- ','(less(X295, X296), delete(X295, X297, X299)).\nand substitutionT6 -> T191,\nX295 -> T191,\nX296 -> T191,\nX297 -> void,\nT7 -> T192,\nX298 -> T192,\nX299 -> T194,\nT3 -> tree(T191, T194, T192),\nT193 -> T194", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 307 [arrowhead = none ];
307 -> 75;

308 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 308 [arrowhead = none ];
308 -> 76;

309 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 309 [arrowhead = none ];
309 -> 49;

310 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 310 [arrowhead = none ];
310 -> 50;

311 [label="EVAL with clause\ndelmin(tree(X172, void, X173), X172, X173).\nand substitutionX172 -> T86,\nX173 -> T87,\nT73 -> tree(T86, void, T87),\nT76 -> T86,\nT77 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 311 [arrowhead = none ];
311 -> 51;

312 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 312 [arrowhead = none ];
312 -> 52;

313 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 313 [arrowhead = none ];
313 -> 54;

314 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 314 [arrowhead = none ];
314 -> 55;

315 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 315 [arrowhead = none ];
315 -> 53;

316 [label="EVAL with clause\ndelmin(tree(X198, X199, X200), X201, tree(X198, X202, X203)) :- delmin(X199, X201, X202).\nand substitutionX198 -> T112,\nX199 -> T113,\nX200 -> T114,\nT73 -> tree(T112, T113, T114),\nT76 -> T118,\nX201 -> T118,\nX202 -> T119,\nX203 -> T117,\nT77 -> tree(T112, T119, T117),\nT115 -> T118,\nT116 -> T119", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 316 [arrowhead = none ];
316 -> 56;

317 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 317 [arrowhead = none ];
317 -> 57;

318 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 318 [arrowhead = none ];
318 -> 66;

319 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
56 -> 319 [arrowhead = none ];
319 -> 58;

320 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 320 [arrowhead = none ];
320 -> 59;

321 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 321 [arrowhead = none ];
321 -> 60;

322 [label="EVAL with clause\ndelmin(tree(X216, void, X217), X216, X217).\nand substitutionX216 -> T132,\nX217 -> T133,\nT113 -> tree(T132, void, T133),\nT118 -> T132,\nT119 -> T133", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 322 [arrowhead = none ];
322 -> 61;

323 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 323 [arrowhead = none ];
323 -> 62;

324 [label="EVAL with clause\ndelmin(tree(X230, X231, X232), X233, tree(X230, X234, X235)) :- delmin(X231, X233, X234).\nand substitutionX230 -> T146,\nX231 -> T147,\nX232 -> T148,\nT113 -> tree(T146, T147, T148),\nT118 -> T152,\nX233 -> T152,\nX234 -> T153,\nX235 -> T151,\nT119 -> tree(T146, T153, T151),\nT149 -> T152,\nT150 -> T153", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 324 [arrowhead = none ];
324 -> 64;

325 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 325 [arrowhead = none ];
325 -> 65;

326 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 326 [arrowhead = none ];
326 -> 63;

327 [label="INSTANCE with matching:\nT113 -> T147\nT118 -> T152\nT119 -> T153", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 327 [arrowhead = none , style=dashed];
327 -> 56[style=dashed];

328 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 328 [arrowhead = none ];
328 -> 67;

329 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 329 [arrowhead = none ];
329 -> 68;

330 [label="EVAL with clause\ndelete(X260, tree(X261, X262, X263), tree(X261, X264, X263)) :- ','(less(X260, X261), delete(X260, X262, X264)).\nand substitutionT72 -> T170,\nX260 -> T170,\nX261 -> T170,\nX262 -> void,\nT73 -> T171,\nX263 -> T171,\nX264 -> T173,\nT3 -> tree(T170, T173, T171),\nT172 -> T173", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 330 [arrowhead = none ];
330 -> 69;

331 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 331 [arrowhead = none ];
331 -> 70;

332 [label="EVAL with clause\ndelete(X277, tree(X278, X279, X280), tree(X278, X279, X281)) :- ','(less(X278, X277), delete(X277, X280, X281)).\nand substitutionT72 -> T180,\nX277 -> T180,\nX278 -> T180,\nX279 -> void,\nT73 -> T181,\nX280 -> T181,\nX281 -> T183,\nT3 -> tree(T180, void, T183),\nT182 -> T183", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 332 [arrowhead = none ];
332 -> 71;

333 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 333 [arrowhead = none ];
333 -> 72;

334 [label="INSTANCE with matching:\nT26 -> T170\nT28 -> T173", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 334 [arrowhead = none , style=dashed];
334 -> 17[style=dashed];

335 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
71 -> 335 [arrowhead = none ];
335 -> 73;

336 [label="SPLIT 2\nnew knowledge:\nT180 is ground", fontsize=14, style = filled, fillcolor = violet];
71 -> 336 [arrowhead = none ];
336 -> 74;

337 [label="INSTANCE with matching:\nT26 -> T180", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 337 [arrowhead = none , style=dashed];
337 -> 19[style=dashed];

338 [label="INSTANCE with matching:\nT1 -> T180\nT2 -> T181\nT3 -> T183", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 338 [arrowhead = none , style=dashed];
338 -> 1[style=dashed];

339 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 339 [arrowhead = none ];
339 -> 77;

340 [label="EVAL with clause\ndelete(X341, tree(X342, X343, X344), tree(X342, X343, X345)) :- ','(less(X342, X341), delete(X341, X344, X345)).\nand substitutionT6 -> T215,\nX341 -> T215,\nX342 -> T215,\nX343 -> void,\nT7 -> T216,\nX344 -> T216,\nX345 -> T218,\nT3 -> tree(T215, void, T218),\nT217 -> T218", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 340 [arrowhead = none ];
340 -> 88;

341 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 341 [arrowhead = none ];
341 -> 89;

342 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 342 [arrowhead = none ];
342 -> 78;

343 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
78 -> 343 [arrowhead = none ];
343 -> 79;

344 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
78 -> 344 [arrowhead = none ];
344 -> 80;

345 [label="EVAL with clause\nless(s(X309), s(X310)) :- less(X309, X310).\nand substitutionX309 -> T199,\nT191 -> s(T199),\nX310 -> T199", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 345 [arrowhead = none ];
345 -> 81;

346 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 346 [arrowhead = none ];
346 -> 82;

347 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 347 [arrowhead = none ];
347 -> 85;

348 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
81 -> 348 [arrowhead = none ];
348 -> 83;

349 [label="SPLIT 2\nnew knowledge:\nT199 is ground", fontsize=14, style = filled, fillcolor = violet];
81 -> 349 [arrowhead = none ];
349 -> 84;

350 [label="INSTANCE with matching:\nT26 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
83 -> 350 [arrowhead = none , style=dashed];
350 -> 19[style=dashed];

351 [label="INSTANCE with matching:\nT1 -> s(T199)\nT2 -> void\nT3 -> T194", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 351 [arrowhead = none , style=dashed];
351 -> 1[style=dashed];

352 [label="EVAL with clause\ndelete(X329, tree(X330, X331, X332), tree(X330, X331, X333)) :- ','(less(X330, X329), delete(X329, X332, X333)).\nand substitutionT191 -> T208,\nX329 -> T208,\nX330 -> T208,\nX331 -> void,\nT192 -> T209,\nX332 -> T209,\nX333 -> T211,\nT3 -> tree(T208, void, T211),\nT210 -> T211", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 352 [arrowhead = none ];
352 -> 86;

353 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 353 [arrowhead = none ];
353 -> 87;

354 [label="INSTANCE with matching:\nT180 -> T208\nT181 -> T209\nT183 -> T211", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 354 [arrowhead = none , style=dashed];
354 -> 71[style=dashed];

355 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
88 -> 355 [arrowhead = none ];
355 -> 90;

356 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 356 [arrowhead = none ];
356 -> 91;

357 [label="EVAL with clause\nless(s(X351), s(X352)) :- less(X351, X352).\nand substitutionX351 -> T221,\nT215 -> s(T221),\nX352 -> T221", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 357 [arrowhead = none ];
357 -> 92;

358 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 358 [arrowhead = none ];
358 -> 93;

359 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
92 -> 359 [arrowhead = none ];
359 -> 94;

360 [label="SPLIT 2\nnew knowledge:\nT221 is ground", fontsize=14, style = filled, fillcolor = violet];
92 -> 360 [arrowhead = none ];
360 -> 95;

361 [label="INSTANCE with matching:\nT26 -> T221", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 361 [arrowhead = none , style=dashed];
361 -> 19[style=dashed];

362 [label="INSTANCE with matching:\nT1 -> s(T221)\nT2 -> T216\nT3 -> T218", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 362 [arrowhead = none , style=dashed];
362 -> 1[style=dashed];

363 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 363 [arrowhead = none ];
363 -> 98;

364 [label="EVAL with clause\ndelete(X509, tree(X509, X510, X511), tree(X512, X510, X513)) :- delmin(X511, X512, X513).\nand substitutionT1 -> T313,\nX509 -> T313,\nX510 -> T314,\nX511 -> T315,\nT2 -> tree(T313, T314, T315),\nX512 -> T318,\nX513 -> T319,\nT3 -> tree(T318, T314, T319),\nT316 -> T318,\nT317 -> T319", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 364 [arrowhead = none ];
364 -> 134;

365 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 365 [arrowhead = none ];
365 -> 135;

366 [label="EVAL with clause\ndelete(X370, tree(X370, X371, X372), tree(X373, X371, X374)) :- delmin(X372, X373, X374).\nand substitutionT228 -> T234,\nX370 -> T234,\nT229 -> T235,\nX371 -> T235,\nX372 -> void,\nX373 -> T238,\nX374 -> T239,\nT3 -> tree(T238, T235, T239),\nT236 -> T238,\nT237 -> T239", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 366 [arrowhead = none ];
366 -> 99;

367 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 367 [arrowhead = none ];
367 -> 100;

368 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
99 -> 368 [arrowhead = none ];
368 -> 101;

369 [label="EVAL with clause\ndelete(X438, tree(X439, X440, X441), tree(X439, X442, X441)) :- ','(less(X438, X439), delete(X438, X440, X442)).\nand substitutionT228 -> T273,\nX438 -> T273,\nX439 -> T273,\nT229 -> T274,\nX440 -> T274,\nX441 -> void,\nX442 -> T276,\nT3 -> tree(T273, T276, void),\nT275 -> T276", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 369 [arrowhead = none ];
369 -> 113;

370 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 370 [arrowhead = none ];
370 -> 114;

371 [label="BACKTRACK\nfor clause: delmin(tree(Y, void, Right), Y, Right)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 371 [arrowhead = none ];
371 -> 102;

372 [label="BACKTRACK\nfor clause: delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 372 [arrowhead = none ];
372 -> 103;

373 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 373 [arrowhead = none ];
373 -> 104;

374 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 374 [arrowhead = none ];
374 -> 105;

375 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 375 [arrowhead = none ];
375 -> 106;

376 [label="EVAL with clause\ndelete(X403, tree(X404, X405, X406), tree(X404, X407, X406)) :- ','(less(X403, X404), delete(X403, X405, X407)).\nand substitutionT234 -> T252,\nX403 -> T252,\nX404 -> T252,\nT235 -> T253,\nX405 -> T253,\nX406 -> void,\nX407 -> T255,\nT3 -> tree(T252, T255, void),\nT254 -> T255", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 376 [arrowhead = none ];
376 -> 107;

377 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 377 [arrowhead = none ];
377 -> 108;

378 [label="EVAL with clause\ndelete(X426, tree(X427, X428, X429), tree(X427, X428, X430)) :- ','(less(X427, X426), delete(X426, X429, X430)).\nand substitutionT234 -> T266,\nX426 -> T266,\nX427 -> T266,\nT235 -> T267,\nX428 -> T267,\nX429 -> void,\nX430 -> T269,\nT3 -> tree(T266, T267, T269),\nT268 -> T269", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 378 [arrowhead = none ];
378 -> 111;

379 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 379 [arrowhead = none ];
379 -> 112;

380 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
107 -> 380 [arrowhead = none ];
380 -> 109;

381 [label="SPLIT 2\nnew knowledge:\nT252 is ground", fontsize=14, style = filled, fillcolor = violet];
107 -> 381 [arrowhead = none ];
381 -> 110;

382 [label="INSTANCE with matching:\nT26 -> T252", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 382 [arrowhead = none , style=dashed];
382 -> 19[style=dashed];

383 [label="INSTANCE with matching:\nT1 -> T252\nT2 -> T253\nT3 -> T255", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 383 [arrowhead = none , style=dashed];
383 -> 1[style=dashed];

384 [label="INSTANCE with matching:\nT26 -> T266\nT28 -> T269", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 384 [arrowhead = none , style=dashed];
384 -> 17[style=dashed];

385 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
113 -> 385 [arrowhead = none ];
385 -> 115;

386 [label="EVAL with clause\ndelete(X484, tree(X485, X486, X487), tree(X485, X486, X488)) :- ','(less(X485, X484), delete(X484, X487, X488)).\nand substitutionT228 -> T299,\nX484 -> T299,\nX485 -> T299,\nT229 -> T300,\nX486 -> T300,\nX487 -> void,\nX488 -> T302,\nT3 -> tree(T299, T300, T302),\nT301 -> T302", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 386 [arrowhead = none ];
386 -> 126;

387 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 387 [arrowhead = none ];
387 -> 127;

388 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 388 [arrowhead = none ];
388 -> 116;

389 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 389 [arrowhead = none ];
389 -> 117;

390 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 390 [arrowhead = none ];
390 -> 118;

391 [label="EVAL with clause\nless(s(X452), s(X453)) :- less(X452, X453).\nand substitutionX452 -> T281,\nT273 -> s(T281),\nX453 -> T281", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 391 [arrowhead = none ];
391 -> 119;

392 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 392 [arrowhead = none ];
392 -> 120;

393 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 393 [arrowhead = none ];
393 -> 123;

394 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
119 -> 394 [arrowhead = none ];
394 -> 121;

395 [label="SPLIT 2\nnew knowledge:\nT281 is ground", fontsize=14, style = filled, fillcolor = violet];
119 -> 395 [arrowhead = none ];
395 -> 122;

396 [label="INSTANCE with matching:\nT26 -> T281", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 396 [arrowhead = none , style=dashed];
396 -> 19[style=dashed];

397 [label="INSTANCE with matching:\nT1 -> s(T281)\nT2 -> T274\nT3 -> T276", fontsize=14, style = filled, fillcolor = lightgrey];
122 -> 397 [arrowhead = none , style=dashed];
397 -> 1[style=dashed];

398 [label="EVAL with clause\ndelete(X472, tree(X473, X474, X475), tree(X473, X474, X476)) :- ','(less(X473, X472), delete(X472, X475, X476)).\nand substitutionT273 -> T292,\nX472 -> T292,\nX473 -> T292,\nT274 -> T293,\nX474 -> T293,\nX475 -> void,\nX476 -> T295,\nT3 -> tree(T292, T293, T295),\nT294 -> T295", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 398 [arrowhead = none ];
398 -> 124;

399 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 399 [arrowhead = none ];
399 -> 125;

400 [label="INSTANCE with matching:\nT26 -> T292\nT28 -> T295", fontsize=14, style = filled, fillcolor = lightgrey];
124 -> 400 [arrowhead = none , style=dashed];
400 -> 17[style=dashed];

401 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
126 -> 401 [arrowhead = none ];
401 -> 128;

402 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 402 [arrowhead = none ];
402 -> 129;

403 [label="EVAL with clause\nless(s(X494), s(X495)) :- less(X494, X495).\nand substitutionX494 -> T305,\nT299 -> s(T305),\nX495 -> T305", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 403 [arrowhead = none ];
403 -> 130;

404 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 404 [arrowhead = none ];
404 -> 131;

405 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
130 -> 405 [arrowhead = none ];
405 -> 132;

406 [label="SPLIT 2\nnew knowledge:\nT305 is ground", fontsize=14, style = filled, fillcolor = violet];
130 -> 406 [arrowhead = none ];
406 -> 133;

407 [label="INSTANCE with matching:\nT26 -> T305", fontsize=14, style = filled, fillcolor = lightgrey];
132 -> 407 [arrowhead = none , style=dashed];
407 -> 19[style=dashed];

408 [label="INSTANCE with matching:\nT1 -> s(T305)\nT2 -> void\nT3 -> T302", fontsize=14, style = filled, fillcolor = lightgrey];
133 -> 408 [arrowhead = none , style=dashed];
408 -> 1[style=dashed];

409 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
134 -> 409 [arrowhead = none ];
409 -> 136;

410 [label="EVAL with clause\ndelete(X619, tree(X620, X621, X622), tree(X620, X623, X622)) :- ','(less(X619, X620), delete(X619, X621, X623)).\nand substitutionT1 -> T413,\nX619 -> T413,\nX620 -> T414,\nX621 -> T415,\nX622 -> T416,\nT2 -> tree(T414, T415, T416),\nX623 -> T418,\nT3 -> tree(T414, T418, T416),\nT417 -> T418", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 410 [arrowhead = none ];
410 -> 157;

411 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 411 [arrowhead = none ];
411 -> 158;

412 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
136 -> 412 [arrowhead = none ];
412 -> 137;

413 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
136 -> 413 [arrowhead = none ];
413 -> 138;

414 [label="EVAL with clause\ndelmin(tree(X522, void, X523), X522, X523).\nand substitutionX522 -> T328,\nX523 -> T329,\nT315 -> tree(T328, void, T329),\nT318 -> T328,\nT319 -> T329", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 414 [arrowhead = none ];
414 -> 139;

415 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 415 [arrowhead = none ];
415 -> 140;

416 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 416 [arrowhead = none ];
416 -> 142;

417 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 417 [arrowhead = none ];
417 -> 143;

418 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 418 [arrowhead = none ];
418 -> 141;

419 [label="EVAL with clause\ndelmin(tree(X548, X549, X550), X551, tree(X548, X552, X553)) :- delmin(X549, X551, X552).\nand substitutionX548 -> T354,\nX549 -> T355,\nX550 -> T356,\nT315 -> tree(T354, T355, T356),\nT318 -> T360,\nX551 -> T360,\nX552 -> T361,\nX553 -> T359,\nT319 -> tree(T354, T361, T359),\nT357 -> T360,\nT358 -> T361", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 419 [arrowhead = none ];
419 -> 144;

420 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
142 -> 420 [arrowhead = none ];
420 -> 145;

421 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 421 [arrowhead = none ];
421 -> 146;

422 [label="INSTANCE with matching:\nT113 -> T355\nT118 -> T360\nT119 -> T361", fontsize=14, style = filled, fillcolor = lightgrey];
144 -> 422 [arrowhead = none , style=dashed];
422 -> 56[style=dashed];

423 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 423 [arrowhead = none ];
423 -> 147;

424 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 424 [arrowhead = none ];
424 -> 148;

425 [label="EVAL with clause\ndelete(X578, tree(X579, X580, X581), tree(X579, X582, X581)) :- ','(less(X578, X579), delete(X578, X580, X582)).\nand substitutionT313 -> T382,\nX578 -> T382,\nX579 -> T382,\nT314 -> T383,\nX580 -> T383,\nT315 -> T384,\nX581 -> T384,\nX582 -> T386,\nT3 -> tree(T382, T386, T384),\nT385 -> T386", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 425 [arrowhead = none ];
425 -> 149;

426 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 426 [arrowhead = none ];
426 -> 150;

427 [label="EVAL with clause\ndelete(X601, tree(X602, X603, X604), tree(X602, X603, X605)) :- ','(less(X602, X601), delete(X601, X604, X605)).\nand substitutionT313 -> T399,\nX601 -> T399,\nX602 -> T399,\nT314 -> T400,\nX603 -> T400,\nT315 -> T401,\nX604 -> T401,\nX605 -> T403,\nT3 -> tree(T399, T400, T403),\nT402 -> T403", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 427 [arrowhead = none ];
427 -> 153;

428 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 428 [arrowhead = none ];
428 -> 154;

429 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
149 -> 429 [arrowhead = none ];
429 -> 151;

430 [label="SPLIT 2\nnew knowledge:\nT382 is ground", fontsize=14, style = filled, fillcolor = violet];
149 -> 430 [arrowhead = none ];
430 -> 152;

431 [label="INSTANCE with matching:\nT26 -> T382", fontsize=14, style = filled, fillcolor = lightgrey];
151 -> 431 [arrowhead = none , style=dashed];
431 -> 19[style=dashed];

432 [label="INSTANCE with matching:\nT1 -> T382\nT2 -> T383\nT3 -> T386", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 432 [arrowhead = none , style=dashed];
432 -> 1[style=dashed];

433 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
153 -> 433 [arrowhead = none ];
433 -> 155;

434 [label="SPLIT 2\nnew knowledge:\nT399 is ground", fontsize=14, style = filled, fillcolor = violet];
153 -> 434 [arrowhead = none ];
434 -> 156;

435 [label="INSTANCE with matching:\nT26 -> T399", fontsize=14, style = filled, fillcolor = lightgrey];
155 -> 435 [arrowhead = none , style=dashed];
435 -> 19[style=dashed];

436 [label="INSTANCE with matching:\nT1 -> T399\nT2 -> T401\nT3 -> T403", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 436 [arrowhead = none , style=dashed];
436 -> 1[style=dashed];

437 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
157 -> 437 [arrowhead = none ];
437 -> 159;

438 [label="EVAL with clause\ndelete(X785, tree(X786, X787, X788), tree(X786, X787, X789)) :- ','(less(X786, X785), delete(X785, X788, X789)).\nand substitutionT1 -> T581,\nX785 -> T581,\nX786 -> T582,\nX787 -> T583,\nX788 -> T584,\nT2 -> tree(T582, T583, T584),\nX789 -> T586,\nT3 -> tree(T582, T583, T586),\nT585 -> T586", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 438 [arrowhead = none ];
438 -> 240;

439 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 439 [arrowhead = none ];
439 -> 241;

440 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
159 -> 440 [arrowhead = none ];
440 -> 160;

441 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
159 -> 441 [arrowhead = none ];
441 -> 161;

442 [label="EVAL with clause\nless(0, s(X628)).\nand substitutionT413 -> 0,\nX628 -> T423,\nT414 -> s(T423)", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 442 [arrowhead = none ];
442 -> 162;

443 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 443 [arrowhead = none ];
443 -> 163;

444 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 444 [arrowhead = none ];
444 -> 164;

445 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 445 [arrowhead = none ];
445 -> 165;

446 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T415\nT3 -> T418", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 446 [arrowhead = none , style=dashed];
446 -> 1[style=dashed];

447 [label="EVAL with clause\nless(s(X641), s(X642)) :- less(X641, X642).\nand substitutionX641 -> T434,\nT413 -> s(T434),\nX642 -> T435,\nT414 -> s(T435)", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 447 [arrowhead = none ];
447 -> 166;

448 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
164 -> 448 [arrowhead = none ];
448 -> 167;

449 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
165 -> 449 [arrowhead = none ];
449 -> 235;

450 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
166 -> 450 [arrowhead = none ];
450 -> 168;

451 [label="SPLIT 2\nnew knowledge:\nT434 is ground\nT435 is ground", fontsize=14, style = filled, fillcolor = violet];
166 -> 451 [arrowhead = none ];
451 -> 169;

452 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
168 -> 452 [arrowhead = none ];
452 -> 170;

453 [label="INSTANCE with matching:\nT1 -> s(T434)\nT2 -> T415\nT3 -> T418", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 453 [arrowhead = none , style=dashed];
453 -> 1[style=dashed];

454 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
170 -> 454 [arrowhead = none ];
454 -> 171;

455 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
170 -> 455 [arrowhead = none ];
455 -> 172;

456 [label="EVAL with clause\nless(0, s(X651)).\nand substitutionT434 -> 0,\nX651 -> T444,\nT435 -> s(T444)", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 456 [arrowhead = none ];
456 -> 173;

457 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
171 -> 457 [arrowhead = none ];
457 -> 174;

458 [label="EVAL with clause\nless(s(X656), s(X657)) :- less(X656, X657).\nand substitutionX656 -> T449,\nT434 -> s(T449),\nX657 -> T450,\nT435 -> s(T450)", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 458 [arrowhead = none ];
458 -> 176;

459 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 459 [arrowhead = none ];
459 -> 177;

460 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 460 [arrowhead = none ];
460 -> 175;

461 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
176 -> 461 [arrowhead = none ];
461 -> 178;

462 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
178 -> 462 [arrowhead = none ];
462 -> 179;

463 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
178 -> 463 [arrowhead = none ];
463 -> 180;

464 [label="EVAL with clause\nless(0, s(X664)).\nand substitutionT449 -> 0,\nX664 -> T457,\nT450 -> s(T457)", fontsize=14, style = filled, fillcolor = lightblue];
179 -> 464 [arrowhead = none ];
464 -> 181;

465 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 465 [arrowhead = none ];
465 -> 182;

466 [label="EVAL with clause\nless(s(X669), s(X670)) :- less(X669, X670).\nand substitutionX669 -> T462,\nT449 -> s(T462),\nX670 -> T463,\nT450 -> s(T463)", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 466 [arrowhead = none ];
466 -> 184;

467 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
180 -> 467 [arrowhead = none ];
467 -> 185;

468 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 468 [arrowhead = none ];
468 -> 183;

469 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
184 -> 469 [arrowhead = none ];
469 -> 186;

470 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
186 -> 470 [arrowhead = none ];
470 -> 187;

471 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
186 -> 471 [arrowhead = none ];
471 -> 188;

472 [label="EVAL with clause\nless(0, s(X677)).\nand substitutionT462 -> 0,\nX677 -> T470,\nT463 -> s(T470)", fontsize=14, style = filled, fillcolor = lightblue];
187 -> 472 [arrowhead = none ];
472 -> 189;

473 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
187 -> 473 [arrowhead = none ];
473 -> 190;

474 [label="EVAL with clause\nless(s(X682), s(X683)) :- less(X682, X683).\nand substitutionX682 -> T475,\nT462 -> s(T475),\nX683 -> T476,\nT463 -> s(T476)", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 474 [arrowhead = none ];
474 -> 192;

475 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
188 -> 475 [arrowhead = none ];
475 -> 193;

476 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 476 [arrowhead = none ];
476 -> 191;

477 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
192 -> 477 [arrowhead = none ];
477 -> 194;

478 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
194 -> 478 [arrowhead = none ];
478 -> 195;

479 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
194 -> 479 [arrowhead = none ];
479 -> 196;

480 [label="EVAL with clause\nless(0, s(X690)).\nand substitutionT475 -> 0,\nX690 -> T483,\nT476 -> s(T483)", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 480 [arrowhead = none ];
480 -> 197;

481 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 481 [arrowhead = none ];
481 -> 198;

482 [label="EVAL with clause\nless(s(X695), s(X696)) :- less(X695, X696).\nand substitutionX695 -> T488,\nT475 -> s(T488),\nX696 -> T489,\nT476 -> s(T489)", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 482 [arrowhead = none ];
482 -> 200;

483 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 483 [arrowhead = none ];
483 -> 201;

484 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 484 [arrowhead = none ];
484 -> 199;

485 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
200 -> 485 [arrowhead = none ];
485 -> 202;

486 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
202 -> 486 [arrowhead = none ];
486 -> 203;

487 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
202 -> 487 [arrowhead = none ];
487 -> 204;

488 [label="EVAL with clause\nless(0, s(X703)).\nand substitutionT488 -> 0,\nX703 -> T496,\nT489 -> s(T496)", fontsize=14, style = filled, fillcolor = lightblue];
203 -> 488 [arrowhead = none ];
488 -> 205;

489 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
203 -> 489 [arrowhead = none ];
489 -> 206;

490 [label="EVAL with clause\nless(s(X708), s(X709)) :- less(X708, X709).\nand substitutionX708 -> T501,\nT488 -> s(T501),\nX709 -> T502,\nT489 -> s(T502)", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 490 [arrowhead = none ];
490 -> 208;

491 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 491 [arrowhead = none ];
491 -> 209;

492 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 492 [arrowhead = none ];
492 -> 207;

493 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
208 -> 493 [arrowhead = none ];
493 -> 210;

494 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
210 -> 494 [arrowhead = none ];
494 -> 211;

495 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
210 -> 495 [arrowhead = none ];
495 -> 212;

496 [label="EVAL with clause\nless(0, s(X716)).\nand substitutionT501 -> 0,\nX716 -> T509,\nT502 -> s(T509)", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 496 [arrowhead = none ];
496 -> 213;

497 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 497 [arrowhead = none ];
497 -> 214;

498 [label="EVAL with clause\nless(s(X721), s(X722)) :- less(X721, X722).\nand substitutionX721 -> T514,\nT501 -> s(T514),\nX722 -> T515,\nT502 -> s(T515)", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 498 [arrowhead = none ];
498 -> 216;

499 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 499 [arrowhead = none ];
499 -> 217;

500 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
213 -> 500 [arrowhead = none ];
500 -> 215;

501 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
216 -> 501 [arrowhead = none ];
501 -> 218;

502 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
218 -> 502 [arrowhead = none ];
502 -> 219;

503 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
218 -> 503 [arrowhead = none ];
503 -> 220;

504 [label="EVAL with clause\nless(0, s(X729)).\nand substitutionT514 -> 0,\nX729 -> T522,\nT515 -> s(T522)", fontsize=14, style = filled, fillcolor = lightblue];
219 -> 504 [arrowhead = none ];
504 -> 221;

505 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
219 -> 505 [arrowhead = none ];
505 -> 222;

506 [label="EVAL with clause\nless(s(X734), s(X735)) :- less(X734, X735).\nand substitutionX734 -> T527,\nT514 -> s(T527),\nX735 -> T528,\nT515 -> s(T528)", fontsize=14, style = filled, fillcolor = lightblue];
220 -> 506 [arrowhead = none ];
506 -> 224;

507 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
220 -> 507 [arrowhead = none ];
507 -> 225;

508 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
221 -> 508 [arrowhead = none ];
508 -> 223;

509 [label="GENERALIZATION\nT531 <-- s(s(s(s(s(s(s(T527)))))))\nT532 <-- s(s(s(s(s(s(s(T528)))))))\n\nNew Knowledge:\nT531 is ground\nT532 is ground", fontsize=14, style = filled, fillcolor = violet];
224 -> 509 [arrowhead = none ];
509 -> 226;

510 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
226 -> 510 [arrowhead = none ];
510 -> 227;

511 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 511 [arrowhead = none ];
511 -> 228;

512 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 512 [arrowhead = none ];
512 -> 229;

513 [label="EVAL with clause\nless(0, s(X744)).\nand substitutionT527 -> 0,\nX744 -> T539,\nT528 -> s(T539)", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 513 [arrowhead = none ];
513 -> 230;

514 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
228 -> 514 [arrowhead = none ];
514 -> 231;

515 [label="EVAL with clause\nless(s(X749), s(X750)) :- less(X749, X750).\nand substitutionX749 -> T544,\nT527 -> s(T544),\nX750 -> T545,\nT528 -> s(T545)", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 515 [arrowhead = none ];
515 -> 233;

516 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
229 -> 516 [arrowhead = none ];
516 -> 234;

517 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
230 -> 517 [arrowhead = none ];
517 -> 232;

518 [label="INSTANCE with matching:\nT527 -> T544\nT528 -> T545", fontsize=14, style = filled, fillcolor = lightgrey];
233 -> 518 [arrowhead = none , style=dashed];
518 -> 226[style=dashed];

519 [label="EVAL with clause\ndelete(X767, tree(X768, X769, X770), tree(X768, X769, X771)) :- ','(less(X768, X767), delete(X767, X770, X771)).\nand substitutionT413 -> T562,\nX767 -> T562,\nT414 -> T563,\nX768 -> T563,\nT415 -> T564,\nX769 -> T564,\nT416 -> T565,\nX770 -> T565,\nX771 -> T567,\nT3 -> tree(T563, T564, T567),\nT566 -> T567", fontsize=14, style = filled, fillcolor = lightblue];
235 -> 519 [arrowhead = none ];
519 -> 236;

520 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
235 -> 520 [arrowhead = none ];
520 -> 237;

521 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
236 -> 521 [arrowhead = none ];
521 -> 238;

522 [label="SPLIT 2\nnew knowledge:\nT563 is ground\nT562 is ground", fontsize=14, style = filled, fillcolor = violet];
236 -> 522 [arrowhead = none ];
522 -> 239;

523 [label="INSTANCE with matching:\nT527 -> T563\nT528 -> T562", fontsize=14, style = filled, fillcolor = lightgrey];
238 -> 523 [arrowhead = none , style=dashed];
523 -> 226[style=dashed];

524 [label="INSTANCE with matching:\nT1 -> T562\nT2 -> T565\nT3 -> T567", fontsize=14, style = filled, fillcolor = lightgrey];
239 -> 524 [arrowhead = none , style=dashed];
524 -> 1[style=dashed];

525 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
240 -> 525 [arrowhead = none ];
525 -> 242;

526 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
242 -> 526 [arrowhead = none ];
526 -> 243;

527 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
242 -> 527 [arrowhead = none ];
527 -> 244;

528 [label="EVAL with clause\nless(0, s(X794)).\nand substitutionT582 -> 0,\nX794 -> T591,\nT581 -> s(T591)", fontsize=14, style = filled, fillcolor = lightblue];
243 -> 528 [arrowhead = none ];
528 -> 245;

529 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
243 -> 529 [arrowhead = none ];
529 -> 246;

530 [label="EVAL with clause\nless(s(X803), s(X804)) :- less(X803, X804).\nand substitutionX803 -> T600,\nT582 -> s(T600),\nX804 -> T601,\nT581 -> s(T601)", fontsize=14, style = filled, fillcolor = lightblue];
244 -> 530 [arrowhead = none ];
530 -> 247;

531 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
244 -> 531 [arrowhead = none ];
531 -> 248;

532 [label="INSTANCE with matching:\nT1 -> s(T591)\nT2 -> T584\nT3 -> T586", fontsize=14, style = filled, fillcolor = lightgrey];
245 -> 532 [arrowhead = none , style=dashed];
532 -> 1[style=dashed];

533 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
247 -> 533 [arrowhead = none ];
533 -> 249;

534 [label="SPLIT 2\nnew knowledge:\nT600 is ground\nT601 is ground", fontsize=14, style = filled, fillcolor = violet];
247 -> 534 [arrowhead = none ];
534 -> 250;

535 [label="INSTANCE with matching:\nT527 -> T600\nT528 -> T601", fontsize=14, style = filled, fillcolor = lightgrey];
249 -> 535 [arrowhead = none , style=dashed];
535 -> 226[style=dashed];

536 [label="INSTANCE with matching:\nT1 -> s(T601)\nT2 -> T584\nT3 -> T586", fontsize=14, style = filled, fillcolor = lightgrey];
250 -> 536 [arrowhead = none , style=dashed];
536 -> 1[style=dashed];

}

(2) Obligation:

Triples:

lessF(s(X1)) :- lessF(X1).
pB(X1, X2) :- lessF(X1).
pB(X1, X2) :- ','(lesscF(X1), deleteA(X1, void, X2)).
pC(X1, X2) :- lessF(X1).
pC(X1, X2) :- ','(lesscF(X1), deleteA(s(X1), void, X2)).
delminD(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delminD(X2, X4, X5).
pE(X1, X2, X3) :- lessF(X1).
pE(X1, X2, X3) :- ','(lesscF(X1), deleteA(X1, X2, X3)).
lessH(s(X1), s(X2)) :- lessH(X1, X2).
deleteA(X1, tree(X1, void, void), tree(X1, X2, void)) :- pB(X1, X2).
deleteA(X1, tree(X1, void, void), tree(X1, void, X2)) :- pB(X1, X2).
deleteA(s(X1), tree(s(X1), void, void), tree(s(X1), X2, void)) :- pC(X1, X2).
deleteA(X1, tree(X1, void, void), tree(X1, void, X2)) :- pB(X1, X2).
deleteA(s(X1), tree(s(X1), void, void), tree(s(X1), void, X2)) :- pC(X1, X2).
deleteA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delminD(X3, X5, X6).
deleteA(X1, tree(X1, void, X2), tree(X1, X3, X2)) :- pB(X1, X3).
deleteA(X1, tree(X1, void, X2), tree(X1, void, X3)) :- pE(X1, X2, X3).
deleteA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) :- lessF(X1).
deleteA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) :- ','(lesscF(X1), deleteA(s(X1), void, X3)).
deleteA(X1, tree(X1, void, X2), tree(X1, void, X3)) :- pE(X1, X2, X3).
deleteA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) :- lessF(X1).
deleteA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) :- ','(lesscF(X1), deleteA(s(X1), X2, X3)).
deleteA(X1, tree(X1, X2, void), tree(X1, X3, void)) :- lessF(X1).
deleteA(X1, tree(X1, X2, void), tree(X1, X3, void)) :- ','(lesscF(X1), deleteA(X1, X2, X3)).
deleteA(X1, tree(X1, X2, void), tree(X1, X2, X3)) :- pB(X1, X3).
deleteA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) :- lessF(X1).
deleteA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) :- ','(lesscF(X1), deleteA(s(X1), X2, X3)).
deleteA(X1, tree(X1, X2, void), tree(X1, X2, X3)) :- pB(X1, X3).
deleteA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) :- lessF(X1).
deleteA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) :- ','(lesscF(X1), deleteA(s(X1), void, X3)).
deleteA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminD(X4, X6, X7).
deleteA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) :- lessF(X1).
deleteA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) :- ','(lesscF(X1), deleteA(X1, X2, X4)).
deleteA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) :- lessF(X1).
deleteA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) :- ','(lesscF(X1), deleteA(X1, X3, X4)).
deleteA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteA(0, X2, X4).
deleteA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) :- lessH(X1, X2).
deleteA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscG(X1, X2), deleteA(s(X1), X3, X5)).
deleteA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- lessH(X2, X1).
deleteA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscH(X2, X1), deleteA(X1, X4, X5)).
deleteA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteA(s(X1), X3, X4).
deleteA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessH(X2, X1).
deleteA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscH(X2, X1), deleteA(s(X1), X4, X5)).

Clauses:

deletecA(X1, tree(X1, void, X2), X2).
deletecA(X1, tree(X1, void, void), void).
deletecA(X1, tree(X1, void, void), tree(X1, X2, void)) :- qcB(X1, X2).
deletecA(X1, tree(X1, void, void), tree(X1, void, X2)) :- qcB(X1, X2).
deletecA(s(X1), tree(s(X1), void, void), tree(s(X1), X2, void)) :- qcC(X1, X2).
deletecA(X1, tree(X1, void, void), tree(X1, void, X2)) :- qcB(X1, X2).
deletecA(s(X1), tree(s(X1), void, void), tree(s(X1), void, X2)) :- qcC(X1, X2).
deletecA(X1, tree(X1, void, tree(X2, void, X3)), tree(X2, void, X3)).
deletecA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delmincD(X3, X5, X6).
deletecA(X1, tree(X1, void, X2), tree(X1, X3, X2)) :- qcB(X1, X3).
deletecA(X1, tree(X1, void, X2), tree(X1, void, X3)) :- qcE(X1, X2, X3).
deletecA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) :- ','(lesscF(X1), deletecA(s(X1), void, X3)).
deletecA(X1, tree(X1, void, X2), tree(X1, void, X3)) :- qcE(X1, X2, X3).
deletecA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) :- ','(lesscF(X1), deletecA(s(X1), X2, X3)).
deletecA(X1, tree(X1, X2, void), X2).
deletecA(X1, tree(X1, X2, void), tree(X1, X3, void)) :- ','(lesscF(X1), deletecA(X1, X2, X3)).
deletecA(X1, tree(X1, X2, void), tree(X1, X2, X3)) :- qcB(X1, X3).
deletecA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) :- ','(lesscF(X1), deletecA(s(X1), X2, X3)).
deletecA(X1, tree(X1, X2, void), tree(X1, X2, X3)) :- qcB(X1, X3).
deletecA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) :- ','(lesscF(X1), deletecA(s(X1), void, X3)).
deletecA(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincD(X4, X6, X7).
deletecA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) :- ','(lesscF(X1), deletecA(X1, X2, X4)).
deletecA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) :- ','(lesscF(X1), deletecA(X1, X3, X4)).
deletecA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecA(0, X2, X4).
deletecA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscG(X1, X2), deletecA(s(X1), X3, X5)).
deletecA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscH(X2, X1), deletecA(X1, X4, X5)).
deletecA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecA(s(X1), X3, X4).
deletecA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscH(X2, X1), deletecA(s(X1), X4, X5)).
lesscF(s(X1)) :- lesscF(X1).
qcB(X1, X2) :- ','(lesscF(X1), deletecA(X1, void, X2)).
qcC(X1, X2) :- ','(lesscF(X1), deletecA(s(X1), void, X2)).
delmincD(tree(X1, void, X2), X1, X2).
delmincD(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delmincD(X2, X4, X5).
qcE(X1, X2, X3) :- ','(lesscF(X1), deletecA(X1, X2, X3)).
lesscH(0, s(X1)).
lesscH(s(X1), s(X2)) :- lesscH(X1, X2).
lesscG(0, s(X1)).
lesscG(s(0), s(s(X1))).
lesscG(s(s(0)), s(s(s(X1)))).
lesscG(s(s(s(0))), s(s(s(s(X1))))).
lesscG(s(s(s(s(0)))), s(s(s(s(s(X1)))))).
lesscG(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))).
lesscG(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))).
lesscG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) :- lesscH(X1, X2).

Afs:

deleteA(x1, x2, x3) = deleteA(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
deleteA_in: (b,b,f)
pB_in: (b,f)
lessF_in: (b)
lesscF_in: (b)
pC_in: (b,f)
delminD_in: (b,f,f)
pE_in: (b,b,f)
lessH_in: (b,b)
lesscG_in: (b,b)
lesscH_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, X2, void)) → U13_GGA(X1, X2, pB_in_ga(X1, X2))
DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, X2, void)) → PB_IN_GA(X1, X2)
PB_IN_GA(X1, X2) → U2_GA(X1, X2, lessF_in_g(X1))
PB_IN_GA(X1, X2) → LESSF_IN_G(X1)
LESSF_IN_G(s(X1)) → U1_G(X1, lessF_in_g(X1))
LESSF_IN_G(s(X1)) → LESSF_IN_G(X1)
PB_IN_GA(X1, X2) → U3_GA(X1, X2, lesscF_in_g(X1))
U3_GA(X1, X2, lesscF_out_g(X1)) → U4_GA(X1, X2, deleteA_in_gga(X1, void, X2))
U3_GA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, void, X2)
DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, void, X2)) → U14_GGA(X1, X2, pB_in_ga(X1, X2))
DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, void, X2)) → PB_IN_GA(X1, X2)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), X2, void)) → U15_GGA(X1, X2, pC_in_ga(X1, X2))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), X2, void)) → PC_IN_GA(X1, X2)
PC_IN_GA(X1, X2) → U5_GA(X1, X2, lessF_in_g(X1))
PC_IN_GA(X1, X2) → LESSF_IN_G(X1)
PC_IN_GA(X1, X2) → U6_GA(X1, X2, lesscF_in_g(X1))
U6_GA(X1, X2, lesscF_out_g(X1)) → U7_GA(X1, X2, deleteA_in_gga(s(X1), void, X2))
U6_GA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), void, X2)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), void, X2)) → U16_GGA(X1, X2, pC_in_ga(X1, X2))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), void, X2)) → PC_IN_GA(X1, X2)
DELETEA_IN_GGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → U17_GGA(X1, X2, X3, X4, X5, X6, X7, delminD_in_gaa(X3, X5, X6))
DELETEA_IN_GGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → DELMIND_IN_GAA(X3, X5, X6)
DELMIND_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U8_GAA(X1, X2, X3, X4, X5, X6, delminD_in_gaa(X2, X4, X5))
DELMIND_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMIND_IN_GAA(X2, X4, X5)
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, X3, X2)) → U18_GGA(X1, X2, X3, pB_in_ga(X1, X3))
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, X3, X2)) → PB_IN_GA(X1, X3)
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, void, X3)) → U19_GGA(X1, X2, X3, pE_in_gga(X1, X2, X3))
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, void, X3)) → PE_IN_GGA(X1, X2, X3)
PE_IN_GGA(X1, X2, X3) → U9_GGA(X1, X2, X3, lessF_in_g(X1))
PE_IN_GGA(X1, X2, X3) → LESSF_IN_G(X1)
PE_IN_GGA(X1, X2, X3) → U10_GGA(X1, X2, X3, lesscF_in_g(X1))
U10_GGA(X1, X2, X3, lesscF_out_g(X1)) → U11_GGA(X1, X2, X3, deleteA_in_gga(X1, X2, X3))
U10_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) → U20_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) → U21_GGA(X1, X2, X3, lesscF_in_g(X1))
U21_GGA(X1, X2, X3, lesscF_out_g(X1)) → U22_GGA(X1, X2, X3, deleteA_in_gga(s(X1), void, X3))
U21_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), void, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) → U23_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) → U24_GGA(X1, X2, X3, lesscF_in_g(X1))
U24_GGA(X1, X2, X3, lesscF_out_g(X1)) → U25_GGA(X1, X2, X3, deleteA_in_gga(s(X1), X2, X3))
U24_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X3, void)) → U26_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X3, void)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X3, void)) → U27_GGA(X1, X2, X3, lesscF_in_g(X1))
U27_GGA(X1, X2, X3, lesscF_out_g(X1)) → U28_GGA(X1, X2, X3, deleteA_in_gga(X1, X2, X3))
U27_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X2, X3)) → U29_GGA(X1, X2, X3, pB_in_ga(X1, X3))
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X2, X3)) → PB_IN_GA(X1, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) → U30_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) → U31_GGA(X1, X2, X3, lesscF_in_g(X1))
U31_GGA(X1, X2, X3, lesscF_out_g(X1)) → U32_GGA(X1, X2, X3, deleteA_in_gga(s(X1), X2, X3))
U31_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) → U33_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) → U34_GGA(X1, X2, X3, lesscF_in_g(X1))
U34_GGA(X1, X2, X3, lesscF_out_g(X1)) → U35_GGA(X1, X2, X3, deleteA_in_gga(s(X1), void, X3))
U34_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), void, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U36_GGA(X1, X2, X3, X4, X5, X6, X7, X8, delminD_in_gaa(X4, X6, X7))
DELETEA_IN_GGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMIND_IN_GAA(X4, X6, X7)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) → U37_GGA(X1, X2, X3, X4, lessF_in_g(X1))
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) → U38_GGA(X1, X2, X3, X4, lesscF_in_g(X1))
U38_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → U39_GGA(X1, X2, X3, X4, deleteA_in_gga(X1, X2, X4))
U38_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X4)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U40_GGA(X1, X2, X3, X4, lessF_in_g(X1))
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U41_GGA(X1, X2, X3, X4, lesscF_in_g(X1))
U41_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → U42_GGA(X1, X2, X3, X4, deleteA_in_gga(X1, X3, X4))
U41_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X3, X4)
DELETEA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U43_GGA(X1, X2, X3, X4, deleteA_in_gga(0, X2, X4))
DELETEA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEA_IN_GGA(0, X2, X4)
DELETEA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → U44_GGA(X1, X2, X3, X4, X5, lessH_in_gg(X1, X2))
DELETEA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → LESSH_IN_GG(X1, X2)
LESSH_IN_GG(s(X1), s(X2)) → U12_GG(X1, X2, lessH_in_gg(X1, X2))
LESSH_IN_GG(s(X1), s(X2)) → LESSH_IN_GG(X1, X2)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U45_GGA(X1, X2, X3, X4, X5, lesscG_in_gg(X1, X2))
U45_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X1, X2)) → U46_GGA(X1, X2, X3, X4, X5, deleteA_in_gga(s(X1), X3, X5))
U45_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X1, X2)) → DELETEA_IN_GGA(s(X1), X3, X5)
DELETEA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U47_GGA(X1, X2, X3, X4, X5, lessH_in_gg(X2, X1))
DELETEA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSH_IN_GG(X2, X1)
DELETEA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U48_GGA(X1, X2, X3, X4, X5, lesscH_in_gg(X2, X1))
U48_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → U49_GGA(X1, X2, X3, X4, X5, deleteA_in_gga(X1, X4, X5))
U48_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(X1, X4, X5)
DELETEA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U50_GGA(X1, X2, X3, X4, deleteA_in_gga(s(X1), X3, X4))
DELETEA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEA_IN_GGA(s(X1), X3, X4)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U51_GGA(X1, X2, X3, X4, X5, lessH_in_gg(X2, X1))
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSH_IN_GG(X2, X1)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U52_GGA(X1, X2, X3, X4, X5, lesscH_in_gg(X2, X1))
U52_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → U53_GGA(X1, X2, X3, X4, X5, deleteA_in_gga(s(X1), X4, X5))
U52_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_g(s(X1)) → U86_g(X1, lesscF_in_g(X1))
U86_g(X1, lesscF_out_g(X1)) → lesscF_out_g(s(X1))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(0), s(s(X1))) → lesscG_out_gg(s(0), s(s(X1)))
lesscG_in_gg(s(s(0)), s(s(s(X1)))) → lesscG_out_gg(s(s(0)), s(s(s(X1))))
lesscG_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscG_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscG_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscG_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscG_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscG_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscG_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscG_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscG_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U95_gg(X1, X2, lesscH_in_gg(X1, X2))
lesscH_in_gg(0, s(X1)) → lesscH_out_gg(0, s(X1))
lesscH_in_gg(s(X1), s(X2)) → U94_gg(X1, X2, lesscH_in_gg(X1, X2))
U94_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscH_out_gg(s(X1), s(X2))
U95_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscG_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))

The argument filtering Pi contains the following mapping:
deleteA_in_gga(x1, x2, x3) = deleteA_in_gga(x1, x2)
tree(x1, x2, x3) = tree(x1, x2, x3)
void = void
pB_in_ga(x1, x2) = pB_in_ga(x1)
lessF_in_g(x1) = lessF_in_g(x1)
s(x1) = s(x1)
lesscF_in_g(x1) = lesscF_in_g(x1)
U86_g(x1, x2) = U86_g(x1, x2)
lesscF_out_g(x1) = lesscF_out_g(x1)
pC_in_ga(x1, x2) = pC_in_ga(x1)
delminD_in_gaa(x1, x2, x3) = delminD_in_gaa(x1)
pE_in_gga(x1, x2, x3) = pE_in_gga(x1, x2)
0 = 0
lessH_in_gg(x1, x2) = lessH_in_gg(x1, x2)
lesscG_in_gg(x1, x2) = lesscG_in_gg(x1, x2)
lesscG_out_gg(x1, x2) = lesscG_out_gg(x1, x2)
U95_gg(x1, x2, x3) = U95_gg(x1, x2, x3)
lesscH_in_gg(x1, x2) = lesscH_in_gg(x1, x2)
lesscH_out_gg(x1, x2) = lesscH_out_gg(x1, x2)
U94_gg(x1, x2, x3) = U94_gg(x1, x2, x3)
DELETEA_IN_GGA(x1, x2, x3) = DELETEA_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3) = U13_GGA(x1, x3)
PB_IN_GA(x1, x2) = PB_IN_GA(x1)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
LESSF_IN_G(x1) = LESSF_IN_G(x1)
U1_G(x1, x2) = U1_G(x1, x2)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
U14_GGA(x1, x2, x3) = U14_GGA(x1, x3)
U15_GGA(x1, x2, x3) = U15_GGA(x1, x3)
PC_IN_GA(x1, x2) = PC_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
U6_GA(x1, x2, x3) = U6_GA(x1, x3)
U7_GA(x1, x2, x3) = U7_GA(x1, x3)
U16_GGA(x1, x2, x3) = U16_GGA(x1, x3)
U17_GGA(x1, x2, x3, x4, x5, x6, x7, x8) = U17_GGA(x1, x2, x3, x4, x8)
DELMIND_IN_GAA(x1, x2, x3) = DELMIND_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5, x6, x7) = U8_GAA(x1, x2, x3, x7)
U18_GGA(x1, x2, x3, x4) = U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4) = U19_GGA(x1, x2, x4)
PE_IN_GGA(x1, x2, x3) = PE_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4) = U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4) = U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4) = U11_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4) = U21_GGA(x1, x2, x4)
U22_GGA(x1, x2, x3, x4) = U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4) = U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4) = U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4) = U25_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4) = U26_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4) = U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4) = U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4) = U30_GGA(x1, x2, x4)
U31_GGA(x1, x2, x3, x4) = U31_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4) = U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4) = U33_GGA(x1, x2, x4)
U34_GGA(x1, x2, x3, x4) = U34_GGA(x1, x2, x4)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x1, x2, x4)
U36_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U36_GGA(x1, x2, x3, x4, x5, x9)
U37_GGA(x1, x2, x3, x4, x5) = U37_GGA(x1, x2, x3, x5)
U38_GGA(x1, x2, x3, x4, x5) = U38_GGA(x1, x2, x3, x5)
U39_GGA(x1, x2, x3, x4, x5) = U39_GGA(x1, x2, x3, x5)
U40_GGA(x1, x2, x3, x4, x5) = U40_GGA(x1, x2, x3, x5)
U41_GGA(x1, x2, x3, x4, x5) = U41_GGA(x1, x2, x3, x5)
U42_GGA(x1, x2, x3, x4, x5) = U42_GGA(x1, x2, x3, x5)
U43_GGA(x1, x2, x3, x4, x5) = U43_GGA(x1, x2, x3, x5)
U44_GGA(x1, x2, x3, x4, x5, x6) = U44_GGA(x1, x2, x3, x4, x6)
LESSH_IN_GG(x1, x2) = LESSH_IN_GG(x1, x2)
U12_GG(x1, x2, x3) = U12_GG(x1, x2, x3)
U45_GGA(x1, x2, x3, x4, x5, x6) = U45_GGA(x1, x2, x3, x4, x6)
U46_GGA(x1, x2, x3, x4, x5, x6) = U46_GGA(x1, x2, x3, x4, x6)
U47_GGA(x1, x2, x3, x4, x5, x6) = U47_GGA(x1, x2, x3, x4, x6)
U48_GGA(x1, x2, x3, x4, x5, x6) = U48_GGA(x1, x2, x3, x4, x6)
U49_GGA(x1, x2, x3, x4, x5, x6) = U49_GGA(x1, x2, x3, x4, x6)
U50_GGA(x1, x2, x3, x4, x5) = U50_GGA(x1, x2, x3, x5)
U51_GGA(x1, x2, x3, x4, x5, x6) = U51_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6) = U52_GGA(x1, x2, x3, x4, x6)
U53_GGA(x1, x2, x3, x4, x5, x6) = U53_GGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, X2, void)) → U13_GGA(X1, X2, pB_in_ga(X1, X2))
DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, X2, void)) → PB_IN_GA(X1, X2)
PB_IN_GA(X1, X2) → U2_GA(X1, X2, lessF_in_g(X1))
PB_IN_GA(X1, X2) → LESSF_IN_G(X1)
LESSF_IN_G(s(X1)) → U1_G(X1, lessF_in_g(X1))
LESSF_IN_G(s(X1)) → LESSF_IN_G(X1)
PB_IN_GA(X1, X2) → U3_GA(X1, X2, lesscF_in_g(X1))
U3_GA(X1, X2, lesscF_out_g(X1)) → U4_GA(X1, X2, deleteA_in_gga(X1, void, X2))
U3_GA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, void, X2)
DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, void, X2)) → U14_GGA(X1, X2, pB_in_ga(X1, X2))
DELETEA_IN_GGA(X1, tree(X1, void, void), tree(X1, void, X2)) → PB_IN_GA(X1, X2)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), X2, void)) → U15_GGA(X1, X2, pC_in_ga(X1, X2))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), X2, void)) → PC_IN_GA(X1, X2)
PC_IN_GA(X1, X2) → U5_GA(X1, X2, lessF_in_g(X1))
PC_IN_GA(X1, X2) → LESSF_IN_G(X1)
PC_IN_GA(X1, X2) → U6_GA(X1, X2, lesscF_in_g(X1))
U6_GA(X1, X2, lesscF_out_g(X1)) → U7_GA(X1, X2, deleteA_in_gga(s(X1), void, X2))
U6_GA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), void, X2)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), void, X2)) → U16_GGA(X1, X2, pC_in_ga(X1, X2))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, void), tree(s(X1), void, X2)) → PC_IN_GA(X1, X2)
DELETEA_IN_GGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → U17_GGA(X1, X2, X3, X4, X5, X6, X7, delminD_in_gaa(X3, X5, X6))
DELETEA_IN_GGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → DELMIND_IN_GAA(X3, X5, X6)
DELMIND_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U8_GAA(X1, X2, X3, X4, X5, X6, delminD_in_gaa(X2, X4, X5))
DELMIND_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMIND_IN_GAA(X2, X4, X5)
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, X3, X2)) → U18_GGA(X1, X2, X3, pB_in_ga(X1, X3))
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, X3, X2)) → PB_IN_GA(X1, X3)
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, void, X3)) → U19_GGA(X1, X2, X3, pE_in_gga(X1, X2, X3))
DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, void, X3)) → PE_IN_GGA(X1, X2, X3)
PE_IN_GGA(X1, X2, X3) → U9_GGA(X1, X2, X3, lessF_in_g(X1))
PE_IN_GGA(X1, X2, X3) → LESSF_IN_G(X1)
PE_IN_GGA(X1, X2, X3) → U10_GGA(X1, X2, X3, lesscF_in_g(X1))
U10_GGA(X1, X2, X3, lesscF_out_g(X1)) → U11_GGA(X1, X2, X3, deleteA_in_gga(X1, X2, X3))
U10_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) → U20_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), X3, X2)) → U21_GGA(X1, X2, X3, lesscF_in_g(X1))
U21_GGA(X1, X2, X3, lesscF_out_g(X1)) → U22_GGA(X1, X2, X3, deleteA_in_gga(s(X1), void, X3))
U21_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), void, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) → U23_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) → U24_GGA(X1, X2, X3, lesscF_in_g(X1))
U24_GGA(X1, X2, X3, lesscF_out_g(X1)) → U25_GGA(X1, X2, X3, deleteA_in_gga(s(X1), X2, X3))
U24_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X3, void)) → U26_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X3, void)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X3, void)) → U27_GGA(X1, X2, X3, lesscF_in_g(X1))
U27_GGA(X1, X2, X3, lesscF_out_g(X1)) → U28_GGA(X1, X2, X3, deleteA_in_gga(X1, X2, X3))
U27_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X2, X3)) → U29_GGA(X1, X2, X3, pB_in_ga(X1, X3))
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X2, X3)) → PB_IN_GA(X1, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) → U30_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) → U31_GGA(X1, X2, X3, lesscF_in_g(X1))
U31_GGA(X1, X2, X3, lesscF_out_g(X1)) → U32_GGA(X1, X2, X3, deleteA_in_gga(s(X1), X2, X3))
U31_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) → U33_GGA(X1, X2, X3, lessF_in_g(X1))
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X2, X3)) → U34_GGA(X1, X2, X3, lesscF_in_g(X1))
U34_GGA(X1, X2, X3, lesscF_out_g(X1)) → U35_GGA(X1, X2, X3, deleteA_in_gga(s(X1), void, X3))
U34_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), void, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U36_GGA(X1, X2, X3, X4, X5, X6, X7, X8, delminD_in_gaa(X4, X6, X7))
DELETEA_IN_GGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMIND_IN_GAA(X4, X6, X7)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) → U37_GGA(X1, X2, X3, X4, lessF_in_g(X1))
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) → U38_GGA(X1, X2, X3, X4, lesscF_in_g(X1))
U38_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → U39_GGA(X1, X2, X3, X4, deleteA_in_gga(X1, X2, X4))
U38_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X4)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U40_GGA(X1, X2, X3, X4, lessF_in_g(X1))
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → LESSF_IN_G(X1)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U41_GGA(X1, X2, X3, X4, lesscF_in_g(X1))
U41_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → U42_GGA(X1, X2, X3, X4, deleteA_in_gga(X1, X3, X4))
U41_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X3, X4)
DELETEA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U43_GGA(X1, X2, X3, X4, deleteA_in_gga(0, X2, X4))
DELETEA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEA_IN_GGA(0, X2, X4)
DELETEA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → U44_GGA(X1, X2, X3, X4, X5, lessH_in_gg(X1, X2))
DELETEA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → LESSH_IN_GG(X1, X2)
LESSH_IN_GG(s(X1), s(X2)) → U12_GG(X1, X2, lessH_in_gg(X1, X2))
LESSH_IN_GG(s(X1), s(X2)) → LESSH_IN_GG(X1, X2)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U45_GGA(X1, X2, X3, X4, X5, lesscG_in_gg(X1, X2))
U45_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X1, X2)) → U46_GGA(X1, X2, X3, X4, X5, deleteA_in_gga(s(X1), X3, X5))
U45_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X1, X2)) → DELETEA_IN_GGA(s(X1), X3, X5)
DELETEA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U47_GGA(X1, X2, X3, X4, X5, lessH_in_gg(X2, X1))
DELETEA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSH_IN_GG(X2, X1)
DELETEA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U48_GGA(X1, X2, X3, X4, X5, lesscH_in_gg(X2, X1))
U48_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → U49_GGA(X1, X2, X3, X4, X5, deleteA_in_gga(X1, X4, X5))
U48_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(X1, X4, X5)
DELETEA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U50_GGA(X1, X2, X3, X4, deleteA_in_gga(s(X1), X3, X4))
DELETEA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEA_IN_GGA(s(X1), X3, X4)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U51_GGA(X1, X2, X3, X4, X5, lessH_in_gg(X2, X1))
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSH_IN_GG(X2, X1)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U52_GGA(X1, X2, X3, X4, X5, lesscH_in_gg(X2, X1))
U52_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → U53_GGA(X1, X2, X3, X4, X5, deleteA_in_gga(s(X1), X4, X5))
U52_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_g(s(X1)) → U86_g(X1, lesscF_in_g(X1))
U86_g(X1, lesscF_out_g(X1)) → lesscF_out_g(s(X1))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(0), s(s(X1))) → lesscG_out_gg(s(0), s(s(X1)))
lesscG_in_gg(s(s(0)), s(s(s(X1)))) → lesscG_out_gg(s(s(0)), s(s(s(X1))))
lesscG_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscG_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscG_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscG_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscG_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscG_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscG_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscG_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscG_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U95_gg(X1, X2, lesscH_in_gg(X1, X2))
lesscH_in_gg(0, s(X1)) → lesscH_out_gg(0, s(X1))
lesscH_in_gg(s(X1), s(X2)) → U94_gg(X1, X2, lesscH_in_gg(X1, X2))
U94_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscH_out_gg(s(X1), s(X2))
U95_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscG_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 69 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSH_IN_GG(s(X1), s(X2)) → LESSH_IN_GG(X1, X2)

The TRS R consists of the following rules:

lesscF_in_g(s(X1)) → U86_g(X1, lesscF_in_g(X1))
U86_g(X1, lesscF_out_g(X1)) → lesscF_out_g(s(X1))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(0), s(s(X1))) → lesscG_out_gg(s(0), s(s(X1)))
lesscG_in_gg(s(s(0)), s(s(s(X1)))) → lesscG_out_gg(s(s(0)), s(s(s(X1))))
lesscG_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscG_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscG_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscG_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscG_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscG_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscG_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscG_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscG_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U95_gg(X1, X2, lesscH_in_gg(X1, X2))
lesscH_in_gg(0, s(X1)) → lesscH_out_gg(0, s(X1))
lesscH_in_gg(s(X1), s(X2)) → U94_gg(X1, X2, lesscH_in_gg(X1, X2))
U94_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscH_out_gg(s(X1), s(X2))
U95_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscG_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSH_IN_GG(s(X1), s(X2)) → LESSH_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSH_IN_GG(s(X1), s(X2)) → LESSH_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LESSH_IN_GG(s(X1), s(X2)) → LESSH_IN_GG(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMIND_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMIND_IN_GAA(X2, X4, X5)

The TRS R consists of the following rules:

lesscF_in_g(s(X1)) → U86_g(X1, lesscF_in_g(X1))
U86_g(X1, lesscF_out_g(X1)) → lesscF_out_g(s(X1))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(0), s(s(X1))) → lesscG_out_gg(s(0), s(s(X1)))
lesscG_in_gg(s(s(0)), s(s(s(X1)))) → lesscG_out_gg(s(s(0)), s(s(s(X1))))
lesscG_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscG_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscG_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscG_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscG_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscG_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscG_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscG_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscG_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U95_gg(X1, X2, lesscH_in_gg(X1, X2))
lesscH_in_gg(0, s(X1)) → lesscH_out_gg(0, s(X1))
lesscH_in_gg(s(X1), s(X2)) → U94_gg(X1, X2, lesscH_in_gg(X1, X2))
U94_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscH_out_gg(s(X1), s(X2))
U95_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscG_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
s(x1) = s(x1)
lesscF_in_g(x1) = lesscF_in_g(x1)
U86_g(x1, x2) = U86_g(x1, x2)
lesscF_out_g(x1) = lesscF_out_g(x1)
0 = 0
lesscG_in_gg(x1, x2) = lesscG_in_gg(x1, x2)
lesscG_out_gg(x1, x2) = lesscG_out_gg(x1, x2)
U95_gg(x1, x2, x3) = U95_gg(x1, x2, x3)
lesscH_in_gg(x1, x2) = lesscH_in_gg(x1, x2)
lesscH_out_gg(x1, x2) = lesscH_out_gg(x1, x2)
U94_gg(x1, x2, x3) = U94_gg(x1, x2, x3)
DELMIND_IN_GAA(x1, x2, x3) = DELMIND_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMIND_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMIND_IN_GAA(X2, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
DELMIND_IN_GAA(x1, x2, x3) = DELMIND_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELMIND_IN_GAA(tree(X1, X2, X3)) → DELMIND_IN_GAA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DELMIND_IN_GAA(tree(X1, X2, X3)) → DELMIND_IN_GAA(X2)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSF_IN_G(s(X1)) → LESSF_IN_G(X1)

The TRS R consists of the following rules:

lesscF_in_g(s(X1)) → U86_g(X1, lesscF_in_g(X1))
U86_g(X1, lesscF_out_g(X1)) → lesscF_out_g(s(X1))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(0), s(s(X1))) → lesscG_out_gg(s(0), s(s(X1)))
lesscG_in_gg(s(s(0)), s(s(s(X1)))) → lesscG_out_gg(s(s(0)), s(s(s(X1))))
lesscG_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscG_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscG_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscG_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscG_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscG_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscG_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscG_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscG_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U95_gg(X1, X2, lesscH_in_gg(X1, X2))
lesscH_in_gg(0, s(X1)) → lesscH_out_gg(0, s(X1))
lesscH_in_gg(s(X1), s(X2)) → U94_gg(X1, X2, lesscH_in_gg(X1, X2))
U94_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscH_out_gg(s(X1), s(X2))
U95_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscG_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSF_IN_G(s(X1)) → LESSF_IN_G(X1)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSF_IN_G(s(X1)) → LESSF_IN_G(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LESSF_IN_G(s(X1)) → LESSF_IN_G(X1)
The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEA_IN_GGA(X1, tree(X1, void, X2), tree(X1, void, X3)) → PE_IN_GGA(X1, X2, X3)
PE_IN_GGA(X1, X2, X3) → U10_GGA(X1, X2, X3, lesscF_in_g(X1))
U10_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2), tree(s(X1), void, X3)) → U24_GGA(X1, X2, X3, lesscF_in_g(X1))
U24_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, void), tree(X1, X3, void)) → U27_GGA(X1, X2, X3, lesscF_in_g(X1))
U27_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X3)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void), tree(s(X1), X3, void)) → U31_GGA(X1, X2, X3, lesscF_in_g(X1))
U31_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2, X3)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X4, X3)) → U38_GGA(X1, X2, X3, X4, lesscF_in_g(X1))
U38_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2, X4)
DELETEA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U41_GGA(X1, X2, X3, X4, lesscF_in_g(X1))
U41_GGA(X1, X2, X3, X4, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X3, X4)
DELETEA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEA_IN_GGA(0, X2, X4)
DELETEA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U48_GGA(X1, X2, X3, X4, X5, lesscH_in_gg(X2, X1))
U48_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(X1, X4, X5)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U45_GGA(X1, X2, X3, X4, X5, lesscG_in_gg(X1, X2))
U45_GGA(X1, X2, X3, X4, X5, lesscG_out_gg(X1, X2)) → DELETEA_IN_GGA(s(X1), X3, X5)
DELETEA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEA_IN_GGA(s(X1), X3, X4)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U52_GGA(X1, X2, X3, X4, X5, lesscH_in_gg(X2, X1))
U52_GGA(X1, X2, X3, X4, X5, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_g(s(X1)) → U86_g(X1, lesscF_in_g(X1))
U86_g(X1, lesscF_out_g(X1)) → lesscF_out_g(s(X1))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(0), s(s(X1))) → lesscG_out_gg(s(0), s(s(X1)))
lesscG_in_gg(s(s(0)), s(s(s(X1)))) → lesscG_out_gg(s(s(0)), s(s(s(X1))))
lesscG_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscG_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscG_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscG_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscG_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscG_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscG_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscG_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscG_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U95_gg(X1, X2, lesscH_in_gg(X1, X2))
lesscH_in_gg(0, s(X1)) → lesscH_out_gg(0, s(X1))
lesscH_in_gg(s(X1), s(X2)) → U94_gg(X1, X2, lesscH_in_gg(X1, X2))
U94_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscH_out_gg(s(X1), s(X2))
U95_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscG_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
void = void
s(x1) = s(x1)
lesscF_in_g(x1) = lesscF_in_g(x1)
U86_g(x1, x2) = U86_g(x1, x2)
lesscF_out_g(x1) = lesscF_out_g(x1)
0 = 0
lesscG_in_gg(x1, x2) = lesscG_in_gg(x1, x2)
lesscG_out_gg(x1, x2) = lesscG_out_gg(x1, x2)
U95_gg(x1, x2, x3) = U95_gg(x1, x2, x3)
lesscH_in_gg(x1, x2) = lesscH_in_gg(x1, x2)
lesscH_out_gg(x1, x2) = lesscH_out_gg(x1, x2)
U94_gg(x1, x2, x3) = U94_gg(x1, x2, x3)
DELETEA_IN_GGA(x1, x2, x3) = DELETEA_IN_GGA(x1, x2)
PE_IN_GGA(x1, x2, x3) = PE_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4) = U10_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4) = U24_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4) = U27_GGA(x1, x2, x4)
U31_GGA(x1, x2, x3, x4) = U31_GGA(x1, x2, x4)
U38_GGA(x1, x2, x3, x4, x5) = U38_GGA(x1, x2, x3, x5)
U41_GGA(x1, x2, x3, x4, x5) = U41_GGA(x1, x2, x3, x5)
U45_GGA(x1, x2, x3, x4, x5, x6) = U45_GGA(x1, x2, x3, x4, x6)
U48_GGA(x1, x2, x3, x4, x5, x6) = U48_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6) = U52_GGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(29) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETEA_IN_GGA(X1, tree(X1, void, X2)) → PE_IN_GGA(X1, X2)
PE_IN_GGA(X1, X2) → U10_GGA(X1, X2, lesscF_in_g(X1))
U10_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2)
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2)) → U24_GGA(X1, X2, lesscF_in_g(X1))
U24_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2)
DELETEA_IN_GGA(X1, tree(X1, X2, void)) → U27_GGA(X1, X2, lesscF_in_g(X1))
U27_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2)
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void)) → U31_GGA(X1, X2, lesscF_in_g(X1))
U31_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2)
DELETEA_IN_GGA(X1, tree(X1, X2, X3)) → U38_GGA(X1, X2, X3, lesscF_in_g(X1))
U38_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2)
DELETEA_IN_GGA(X1, tree(X1, X2, X3)) → U41_GGA(X1, X2, X3, lesscF_in_g(X1))
U41_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X3)
DELETEA_IN_GGA(0, tree(s(X1), X2, X3)) → DELETEA_IN_GGA(0, X2)
DELETEA_IN_GGA(X1, tree(X2, X3, X4)) → U48_GGA(X1, X2, X3, X4, lesscH_in_gg(X2, X1))
U48_GGA(X1, X2, X3, X4, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(X1, X4)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4)) → U45_GGA(X1, X2, X3, X4, lesscG_in_gg(X1, X2))
U45_GGA(X1, X2, X3, X4, lesscG_out_gg(X1, X2)) → DELETEA_IN_GGA(s(X1), X3)
DELETEA_IN_GGA(s(X1), tree(0, X2, X3)) → DELETEA_IN_GGA(s(X1), X3)
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4)) → U52_GGA(X1, X2, X3, X4, lesscH_in_gg(X2, X1))
U52_GGA(X1, X2, X3, X4, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(s(X1), X4)

The TRS R consists of the following rules:

lesscF_in_g(s(X1)) → U86_g(X1, lesscF_in_g(X1))
U86_g(X1, lesscF_out_g(X1)) → lesscF_out_g(s(X1))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(0), s(s(X1))) → lesscG_out_gg(s(0), s(s(X1)))
lesscG_in_gg(s(s(0)), s(s(s(X1)))) → lesscG_out_gg(s(s(0)), s(s(s(X1))))
lesscG_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscG_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscG_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscG_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscG_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscG_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscG_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscG_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscG_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U95_gg(X1, X2, lesscH_in_gg(X1, X2))
lesscH_in_gg(0, s(X1)) → lesscH_out_gg(0, s(X1))
lesscH_in_gg(s(X1), s(X2)) → U94_gg(X1, X2, lesscH_in_gg(X1, X2))
U94_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscH_out_gg(s(X1), s(X2))
U95_gg(X1, X2, lesscH_out_gg(X1, X2)) → lesscG_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))

The set Q consists of the following terms:

lesscF_in_g(x0)
U86_g(x0, x1)
lesscG_in_gg(x0, x1)
lesscH_in_gg(x0, x1)
U94_gg(x0, x1, x2)
U95_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(31) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

PE_IN_GGA(X1, X2) → U10_GGA(X1, X2, lesscF_in_g(X1))
The graph contains the following edges 1 >= 1, 2 >= 2
U10_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2
DELETEA_IN_GGA(X1, tree(X1, void, X2)) → PE_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
DELETEA_IN_GGA(s(X1), tree(0, X2, X3)) → DELETEA_IN_GGA(s(X1), X3)
The graph contains the following edges 1 >= 1, 2 > 2
DELETEA_IN_GGA(0, tree(s(X1), X2, X3)) → DELETEA_IN_GGA(0, X2)
The graph contains the following edges 1 >= 1, 2 > 2
U24_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2)
The graph contains the following edges 2 >= 2
DELETEA_IN_GGA(s(X1), tree(s(X1), void, X2)) → U24_GGA(X1, X2, lesscF_in_g(X1))
The graph contains the following edges 1 > 1, 2 > 1, 2 > 2
U27_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2
DELETEA_IN_GGA(X1, tree(X1, X2, void)) → U27_GGA(X1, X2, lesscF_in_g(X1))
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
U31_GGA(X1, X2, lesscF_out_g(X1)) → DELETEA_IN_GGA(s(X1), X2)
The graph contains the following edges 2 >= 2
DELETEA_IN_GGA(s(X1), tree(s(X1), X2, void)) → U31_GGA(X1, X2, lesscF_in_g(X1))
The graph contains the following edges 1 > 1, 2 > 1, 2 > 2
U38_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 4 > 1, 2 >= 2
DELETEA_IN_GGA(X1, tree(X1, X2, X3)) → U38_GGA(X1, X2, X3, lesscF_in_g(X1))
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 2 > 3
U41_GGA(X1, X2, X3, lesscF_out_g(X1)) → DELETEA_IN_GGA(X1, X3)
The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2
DELETEA_IN_GGA(X1, tree(X1, X2, X3)) → U41_GGA(X1, X2, X3, lesscF_in_g(X1))
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 2 > 3
U48_GGA(X1, X2, X3, X4, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(X1, X4)
The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2
DELETEA_IN_GGA(X1, tree(X2, X3, X4)) → U48_GGA(X1, X2, X3, X4, lesscH_in_gg(X2, X1))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4
U45_GGA(X1, X2, X3, X4, lesscG_out_gg(X1, X2)) → DELETEA_IN_GGA(s(X1), X3)
The graph contains the following edges 3 >= 2
U52_GGA(X1, X2, X3, X4, lesscH_out_gg(X2, X1)) → DELETEA_IN_GGA(s(X1), X4)
The graph contains the following edges 4 >= 2
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4)) → U45_GGA(X1, X2, X3, X4, lesscG_in_gg(X1, X2))
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3, 2 > 4
DELETEA_IN_GGA(s(X1), tree(s(X2), X3, X4)) → U52_GGA(X1, X2, X3, X4, lesscH_in_gg(X2, X1))
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3, 2 > 4

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) PiDPToQDPProof (SOUND transformation)

(30) Obligation:

(31) QDPSizeChangeProof (EQUIVALENT transformation)

(32) YES